Termination proof of /tmp/tmp1F0ati/DuplicateTreePath.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBC2FIG (⇐)

↳2 FIGraph

↳3 FIGtoITRSProof (⇐)

↳4 AND

    ↳5 ITRS

        ↳6 ITRStoIDPProof (⇔)

        ↳7 IDP

        ↳8 UsableRulesProof (⇔)

        ↳9 IDP

        ↳10 ItpfGraphProof (⇔)

        ↳11 IDP

        ↳12 IDPNonInfProof (⇐)

        ↳13 AND

            ↳14 IDP

                ↳15 IDependencyGraphProof (⇔)

                ↳16 TRUE

            ↳17 IDP

                ↳18 IDependencyGraphProof (⇔)

                ↳19 TRUE

    ↳20 ITRS

        ↳21 DuplicateArgsRemoverProof (⇔)

        ↳22 ITRS

        ↳23 ITRSFilterProcessorProof (⇐)

        ↳24 ITRS

        ↳25 ITRSFSMergerProof (⇐)

        ↳26 ITRS

        ↳27 ITRStoIDPProof (⇔)

        ↳28 IDP

        ↳29 UsableRulesProof (⇔)

        ↳30 IDP

        ↳31 ItpfGraphProof (⇔)

        ↳32 IDP

        ↳33 IDPNonInfProof (⇐)

        ↳34 AND

            ↳35 IDP

                ↳36 IDependencyGraphProof (⇔)

                ↳37 TRUE

            ↳38 IDP

                ↳39 IDependencyGraphProof (⇔)

                ↳40 TRUE

(0) Obligation:

JBC Problem based on JBC Program:

No human-readable program information known.

Manifest-Version: 1.0 Created-By: 1.6.0_20 (Sun Microsystems Inc.) Main-Class: DuplicateTreePath

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Graph of 497 nodes with 2 SCCs.

(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph to ITRS rules

(4) Complex Obligation (AND)

(5) Obligation:

ITRS problem:

The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Load13105(java.lang.Object(ARRAY(i2, a7588data)), i1876, java.lang.Object(Tree(o8359, java.lang.Object(Tree(o8442Field0, o8442Field1, o8442Field2)), o8361))) → Load12814(java.lang.Object(ARRAY(i2, a7588data)), i1876, java.lang.Object(Tree(o8442Field0, o8442Field1, o8442Field2)))
Load12814(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(o8359, java.lang.Object(Tree(o8442Field0, o8442Field1, o8442Field2)), o8361))) → Load12814ARR1(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(o8359, java.lang.Object(Tree(o8442Field0, o8442Field1, o8442Field2)), o8361)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876)))
Load12814ARR1(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359, java.lang.Object(Tree(o8442Field0, o8442Field1, o8442Field2)), o8361)), o8361)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876))) → Cond_Load12814ARR1(i1942 >= 42 && i1840 > 0 && i1840 < i2 && i1840 + 1 > 0, java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359, java.lang.Object(Tree(o8442Field0, o8442Field1, o8442Field2)), o8361)), o8361)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876)))
Cond_Load12814ARR1(TRUE, java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359, java.lang.Object(Tree(o8442Field0, o8442Field1, o8442Field2)), o8361)), o8361)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876))) → Load12814(java.lang.Object(ARRAY(i2, a7588data)), i1840 + 1, java.lang.Object(Tree(o8442Field0, o8442Field1, o8442Field2)))
Load12814(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0, o8443Field1, o8443Field2)), o8366, o8367))) → Load12814ARR2(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0, o8443Field1, o8443Field2)), o8366, o8367)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876)))
Load12814ARR2(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0, o8443Field1, o8443Field2)), o8366, o8367)), NULL, o8367)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876))) → Cond_Load12814ARR2(i1942 >= 0 && i1942 < 42 && i1840 > 0 && i1840 < i2 && i1840 + 1 > 0, java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0, o8443Field1, o8443Field2)), o8366, o8367)), NULL, o8367)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876)))
Cond_Load12814ARR2(TRUE, java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0, o8443Field1, o8443Field2)), o8366, o8367)), NULL, o8367)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876))) → Load12814(java.lang.Object(ARRAY(i2, a7588data)), i1840 + 1, java.lang.Object(Tree(o8443Field0, o8443Field1, o8443Field2)))
Load12814(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(NULL, o8366, o8367))) → Load12814ARR3(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(NULL, o8366, o8367)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876)))
Load12814ARR3(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(NULL, o8366, o8367)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876))) → Cond_Load12814ARR3(i1942 >= 0 && i1942 < 42 && i1840 > 0 && i1840 < i2 && i1840 + 1 > 0, java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(NULL, o8366, o8367)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876)))
Cond_Load12814ARR3(TRUE, java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(NULL, o8366, o8367)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876))) → Load13105(java.lang.Object(ARRAY(i2, a7588data)), i1840 + 1, java.lang.Object(Tree(NULL, o8366, o8367)))
The set Q consists of the following terms:
Load13105(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(x3, java.lang.Object(Tree(x4, x5, x6)), x7)))
Load12814(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(x3, java.lang.Object(Tree(x4, x5, x6)), x7)))
Load12814ARR1(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(NULL, java.lang.Object(Tree(x3, java.lang.Object(Tree(x4, x5, x6)), x7)), x7)), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
Cond_Load12814ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(NULL, java.lang.Object(Tree(x3, java.lang.Object(Tree(x4, x5, x6)), x7)), x7)), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
Load12814(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(java.lang.Object(Tree(x3, x4, x5)), x6, x7)))
Load12814ARR2(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x3, x4, x5)), x6, x7)), NULL, x7)), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
Cond_Load12814ARR2(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x3, x4, x5)), x6, x7)), NULL, x7)), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
Load12814(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(NULL, x3, x4)))
Load12814ARR3(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(NULL, x3, x4)), java.lang.Object(java.lang.String(x5, x6, x7, x8)))
Cond_Load12814ARR3(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(NULL, x3, x4)), java.lang.Object(java.lang.String(x5, x6, x7, x8)))

(6) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

(7) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

The ITRS R consists of the following rules:
Load13105(java.lang.Object(ARRAY(i2, a7588data)), i1876, java.lang.Object(Tree(o8359, java.lang.Object(Tree(o8442Field0, o8442Field1, o8442Field2)), o8361))) → Load12814(java.lang.Object(ARRAY(i2, a7588data)), i1876, java.lang.Object(Tree(o8442Field0, o8442Field1, o8442Field2)))
Load12814(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(o8359, java.lang.Object(Tree(o8442Field0, o8442Field1, o8442Field2)), o8361))) → Load12814ARR1(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(o8359, java.lang.Object(Tree(o8442Field0, o8442Field1, o8442Field2)), o8361)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876)))
Load12814ARR1(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359, java.lang.Object(Tree(o8442Field0, o8442Field1, o8442Field2)), o8361)), o8361)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876))) → Cond_Load12814ARR1(i1942 >= 42 && i1840 > 0 && i1840 < i2 && i1840 + 1 > 0, java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359, java.lang.Object(Tree(o8442Field0, o8442Field1, o8442Field2)), o8361)), o8361)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876)))
Cond_Load12814ARR1(TRUE, java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359, java.lang.Object(Tree(o8442Field0, o8442Field1, o8442Field2)), o8361)), o8361)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876))) → Load12814(java.lang.Object(ARRAY(i2, a7588data)), i1840 + 1, java.lang.Object(Tree(o8442Field0, o8442Field1, o8442Field2)))
Load12814(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0, o8443Field1, o8443Field2)), o8366, o8367))) → Load12814ARR2(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0, o8443Field1, o8443Field2)), o8366, o8367)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876)))
Load12814ARR2(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0, o8443Field1, o8443Field2)), o8366, o8367)), NULL, o8367)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876))) → Cond_Load12814ARR2(i1942 >= 0 && i1942 < 42 && i1840 > 0 && i1840 < i2 && i1840 + 1 > 0, java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0, o8443Field1, o8443Field2)), o8366, o8367)), NULL, o8367)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876)))
Cond_Load12814ARR2(TRUE, java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0, o8443Field1, o8443Field2)), o8366, o8367)), NULL, o8367)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876))) → Load12814(java.lang.Object(ARRAY(i2, a7588data)), i1840 + 1, java.lang.Object(Tree(o8443Field0, o8443Field1, o8443Field2)))
Load12814(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(NULL, o8366, o8367))) → Load12814ARR3(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(NULL, o8366, o8367)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876)))
Load12814ARR3(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(NULL, o8366, o8367)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876))) → Cond_Load12814ARR3(i1942 >= 0 && i1942 < 42 && i1840 > 0 && i1840 < i2 && i1840 + 1 > 0, java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(NULL, o8366, o8367)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876)))
Cond_Load12814ARR3(TRUE, java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(NULL, o8366, o8367)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876))) → Load13105(java.lang.Object(ARRAY(i2, a7588data)), i1840 + 1, java.lang.Object(Tree(NULL, o8366, o8367)))

The integer pair graph contains the following rules and edges:
(0): LOAD13105(java.lang.Object(ARRAY(i2[0], a7588data[0])), i1876[0], java.lang.Object(Tree(o8359[0], java.lang.Object(Tree(o8442Field0[0], o8442Field1[0], o8442Field2[0])), o8361[0]))) → LOAD12814(java.lang.Object(ARRAY(i2[0], a7588data[0])), i1876[0], java.lang.Object(Tree(o8442Field0[0], o8442Field1[0], o8442Field2[0])))
(1): LOAD12814(java.lang.Object(ARRAY(i2[1], a7588data[1])), i1840[1], java.lang.Object(Tree(o8359[1], java.lang.Object(Tree(o8442Field0[1], o8442Field1[1], o8442Field2[1])), o8361[1]))) → LOAD12814ARR1(java.lang.Object(ARRAY(i2[1], a7588data[1])), i1840[1], java.lang.Object(Tree(o8359[1], java.lang.Object(Tree(o8442Field0[1], o8442Field1[1], o8442Field2[1])), o8361[1])), java.lang.Object(java.lang.String(i1942[1], i1941[1], i1943[1], a7876[1])))
(2): LOAD12814ARR1(java.lang.Object(ARRAY(i2[2], a7588data[2])), i1840[2], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[2], java.lang.Object(Tree(o8442Field0[2], o8442Field1[2], o8442Field2[2])), o8361[2])), o8361[2])), java.lang.Object(java.lang.String(i1942[2], i1941[2], i1943[2], a7876[2]))) → COND_LOAD12814ARR1(i1942[2] >= 42 && i1840[2] > 0 && i1840[2] < i2[2] && i1840[2] + 1 > 0, java.lang.Object(ARRAY(i2[2], a7588data[2])), i1840[2], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[2], java.lang.Object(Tree(o8442Field0[2], o8442Field1[2], o8442Field2[2])), o8361[2])), o8361[2])), java.lang.Object(java.lang.String(i1942[2], i1941[2], i1943[2], a7876[2])))
(3): COND_LOAD12814ARR1(TRUE, java.lang.Object(ARRAY(i2[3], a7588data[3])), i1840[3], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[3], java.lang.Object(Tree(o8442Field0[3], o8442Field1[3], o8442Field2[3])), o8361[3])), o8361[3])), java.lang.Object(java.lang.String(i1942[3], i1941[3], i1943[3], a7876[3]))) → LOAD12814(java.lang.Object(ARRAY(i2[3], a7588data[3])), i1840[3] + 1, java.lang.Object(Tree(o8442Field0[3], o8442Field1[3], o8442Field2[3])))
(4): LOAD12814(java.lang.Object(ARRAY(i2[4], a7588data[4])), i1840[4], java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[4], o8443Field1[4], o8443Field2[4])), o8366[4], o8367[4]))) → LOAD12814ARR2(java.lang.Object(ARRAY(i2[4], a7588data[4])), i1840[4], java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[4], o8443Field1[4], o8443Field2[4])), o8366[4], o8367[4])), java.lang.Object(java.lang.String(i1942[4], i1941[4], i1943[4], a7876[4])))
(5): LOAD12814ARR2(java.lang.Object(ARRAY(i2[5], a7588data[5])), i1840[5], java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[5], o8443Field1[5], o8443Field2[5])), o8366[5], o8367[5])), NULL, o8367[5])), java.lang.Object(java.lang.String(i1942[5], i1941[5], i1943[5], a7876[5]))) → COND_LOAD12814ARR2(i1942[5] >= 0 && i1942[5] < 42 && i1840[5] > 0 && i1840[5] < i2[5] && i1840[5] + 1 > 0, java.lang.Object(ARRAY(i2[5], a7588data[5])), i1840[5], java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[5], o8443Field1[5], o8443Field2[5])), o8366[5], o8367[5])), NULL, o8367[5])), java.lang.Object(java.lang.String(i1942[5], i1941[5], i1943[5], a7876[5])))
(6): COND_LOAD12814ARR2(TRUE, java.lang.Object(ARRAY(i2[6], a7588data[6])), i1840[6], java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[6], o8443Field1[6], o8443Field2[6])), o8366[6], o8367[6])), NULL, o8367[6])), java.lang.Object(java.lang.String(i1942[6], i1941[6], i1943[6], a7876[6]))) → LOAD12814(java.lang.Object(ARRAY(i2[6], a7588data[6])), i1840[6] + 1, java.lang.Object(Tree(o8443Field0[6], o8443Field1[6], o8443Field2[6])))
(7): LOAD12814(java.lang.Object(ARRAY(i2[7], a7588data[7])), i1840[7], java.lang.Object(Tree(NULL, o8366[7], o8367[7]))) → LOAD12814ARR3(java.lang.Object(ARRAY(i2[7], a7588data[7])), i1840[7], java.lang.Object(Tree(NULL, o8366[7], o8367[7])), java.lang.Object(java.lang.String(i1942[7], i1941[7], i1943[7], a7876[7])))
(8): LOAD12814ARR3(java.lang.Object(ARRAY(i2[8], a7588data[8])), i1840[8], java.lang.Object(Tree(NULL, o8366[8], o8367[8])), java.lang.Object(java.lang.String(i1942[8], i1941[8], i1943[8], a7876[8]))) → COND_LOAD12814ARR3(i1942[8] >= 0 && i1942[8] < 42 && i1840[8] > 0 && i1840[8] < i2[8] && i1840[8] + 1 > 0, java.lang.Object(ARRAY(i2[8], a7588data[8])), i1840[8], java.lang.Object(Tree(NULL, o8366[8], o8367[8])), java.lang.Object(java.lang.String(i1942[8], i1941[8], i1943[8], a7876[8])))
(9): COND_LOAD12814ARR3(TRUE, java.lang.Object(ARRAY(i2[9], a7588data[9])), i1840[9], java.lang.Object(Tree(NULL, o8366[9], o8367[9])), java.lang.Object(java.lang.String(i1942[9], i1941[9], i1943[9], a7876[9]))) → LOAD13105(java.lang.Object(ARRAY(i2[9], a7588data[9])), i1840[9] + 1, java.lang.Object(Tree(NULL, o8366[9], o8367[9])))

(0) -> (1), if ((java.lang.Object(ARRAY(i2[0], a7588data[0])) →^* java.lang.Object(ARRAY(i2[1], a7588data[1])))∧(i1876[0] →^* i1840[1])∧(java.lang.Object(Tree(o8442Field0[0], o8442Field1[0], o8442Field2[0])) →^* java.lang.Object(Tree(o8359[1], java.lang.Object(Tree(o8442Field0[1], o8442Field1[1], o8442Field2[1])), o8361[1]))))

(0) -> (4), if ((i1876[0] →^* i1840[4])∧(java.lang.Object(Tree(o8442Field0[0], o8442Field1[0], o8442Field2[0])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[4], o8443Field1[4], o8443Field2[4])), o8366[4], o8367[4])))∧(java.lang.Object(ARRAY(i2[0], a7588data[0])) →^* java.lang.Object(ARRAY(i2[4], a7588data[4]))))

(0) -> (7), if ((java.lang.Object(ARRAY(i2[0], a7588data[0])) →^* java.lang.Object(ARRAY(i2[7], a7588data[7])))∧(i1876[0] →^* i1840[7])∧(java.lang.Object(Tree(o8442Field0[0], o8442Field1[0], o8442Field2[0])) →^* java.lang.Object(Tree(NULL, o8366[7], o8367[7]))))

(1) -> (2), if ((java.lang.Object(java.lang.String(i1942[1], i1941[1], i1943[1], a7876[1])) →^* java.lang.Object(java.lang.String(i1942[2], i1941[2], i1943[2], a7876[2])))∧(java.lang.Object(ARRAY(i2[1], a7588data[1])) →^* java.lang.Object(ARRAY(i2[2], a7588data[2])))∧(java.lang.Object(Tree(o8359[1], java.lang.Object(Tree(o8442Field0[1], o8442Field1[1], o8442Field2[1])), o8361[1])) →^* java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[2], java.lang.Object(Tree(o8442Field0[2], o8442Field1[2], o8442Field2[2])), o8361[2])), o8361[2])))∧(i1840[1] →^* i1840[2]))

(2) -> (3), if ((java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[2], java.lang.Object(Tree(o8442Field0[2], o8442Field1[2], o8442Field2[2])), o8361[2])), o8361[2])) →^* java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[3], java.lang.Object(Tree(o8442Field0[3], o8442Field1[3], o8442Field2[3])), o8361[3])), o8361[3])))∧(i1942[2] >= 42 && i1840[2] > 0 && i1840[2] < i2[2] && i1840[2] + 1 > 0 →^* TRUE)∧(java.lang.Object(java.lang.String(i1942[2], i1941[2], i1943[2], a7876[2])) →^* java.lang.Object(java.lang.String(i1942[3], i1941[3], i1943[3], a7876[3])))∧(i1840[2] →^* i1840[3])∧(java.lang.Object(ARRAY(i2[2], a7588data[2])) →^* java.lang.Object(ARRAY(i2[3], a7588data[3]))))

(3) -> (1), if ((java.lang.Object(ARRAY(i2[3], a7588data[3])) →^* java.lang.Object(ARRAY(i2[1], a7588data[1])))∧(i1840[3] + 1 →^* i1840[1])∧(java.lang.Object(Tree(o8442Field0[3], o8442Field1[3], o8442Field2[3])) →^* java.lang.Object(Tree(o8359[1], java.lang.Object(Tree(o8442Field0[1], o8442Field1[1], o8442Field2[1])), o8361[1]))))

(3) -> (4), if ((java.lang.Object(Tree(o8442Field0[3], o8442Field1[3], o8442Field2[3])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[4], o8443Field1[4], o8443Field2[4])), o8366[4], o8367[4])))∧(i1840[3] + 1 →^* i1840[4])∧(java.lang.Object(ARRAY(i2[3], a7588data[3])) →^* java.lang.Object(ARRAY(i2[4], a7588data[4]))))

(3) -> (7), if ((i1840[3] + 1 →^* i1840[7])∧(java.lang.Object(Tree(o8442Field0[3], o8442Field1[3], o8442Field2[3])) →^* java.lang.Object(Tree(NULL, o8366[7], o8367[7])))∧(java.lang.Object(ARRAY(i2[3], a7588data[3])) →^* java.lang.Object(ARRAY(i2[7], a7588data[7]))))

(4) -> (5), if ((java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[4], o8443Field1[4], o8443Field2[4])), o8366[4], o8367[4])) →^* java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[5], o8443Field1[5], o8443Field2[5])), o8366[5], o8367[5])), NULL, o8367[5])))∧(i1840[4] →^* i1840[5])∧(java.lang.Object(java.lang.String(i1942[4], i1941[4], i1943[4], a7876[4])) →^* java.lang.Object(java.lang.String(i1942[5], i1941[5], i1943[5], a7876[5])))∧(java.lang.Object(ARRAY(i2[4], a7588data[4])) →^* java.lang.Object(ARRAY(i2[5], a7588data[5]))))

(5) -> (6), if ((java.lang.Object(java.lang.String(i1942[5], i1941[5], i1943[5], a7876[5])) →^* java.lang.Object(java.lang.String(i1942[6], i1941[6], i1943[6], a7876[6])))∧(java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[5], o8443Field1[5], o8443Field2[5])), o8366[5], o8367[5])), NULL, o8367[5])) →^* java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[6], o8443Field1[6], o8443Field2[6])), o8366[6], o8367[6])), NULL, o8367[6])))∧(i1840[5] →^* i1840[6])∧(java.lang.Object(ARRAY(i2[5], a7588data[5])) →^* java.lang.Object(ARRAY(i2[6], a7588data[6])))∧(i1942[5] >= 0 && i1942[5] < 42 && i1840[5] > 0 && i1840[5] < i2[5] && i1840[5] + 1 > 0 →^* TRUE))

(6) -> (1), if ((i1840[6] + 1 →^* i1840[1])∧(java.lang.Object(ARRAY(i2[6], a7588data[6])) →^* java.lang.Object(ARRAY(i2[1], a7588data[1])))∧(java.lang.Object(Tree(o8443Field0[6], o8443Field1[6], o8443Field2[6])) →^* java.lang.Object(Tree(o8359[1], java.lang.Object(Tree(o8442Field0[1], o8442Field1[1], o8442Field2[1])), o8361[1]))))

(6) -> (4), if ((java.lang.Object(ARRAY(i2[6], a7588data[6])) →^* java.lang.Object(ARRAY(i2[4], a7588data[4])))∧(i1840[6] + 1 →^* i1840[4])∧(java.lang.Object(Tree(o8443Field0[6], o8443Field1[6], o8443Field2[6])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[4], o8443Field1[4], o8443Field2[4])), o8366[4], o8367[4]))))

(6) -> (7), if ((java.lang.Object(ARRAY(i2[6], a7588data[6])) →^* java.lang.Object(ARRAY(i2[7], a7588data[7])))∧(java.lang.Object(Tree(o8443Field0[6], o8443Field1[6], o8443Field2[6])) →^* java.lang.Object(Tree(NULL, o8366[7], o8367[7])))∧(i1840[6] + 1 →^* i1840[7]))

(7) -> (8), if ((java.lang.Object(java.lang.String(i1942[7], i1941[7], i1943[7], a7876[7])) →^* java.lang.Object(java.lang.String(i1942[8], i1941[8], i1943[8], a7876[8])))∧(i1840[7] →^* i1840[8])∧(java.lang.Object(ARRAY(i2[7], a7588data[7])) →^* java.lang.Object(ARRAY(i2[8], a7588data[8])))∧(java.lang.Object(Tree(NULL, o8366[7], o8367[7])) →^* java.lang.Object(Tree(NULL, o8366[8], o8367[8]))))

(8) -> (9), if ((i1942[8] >= 0 && i1942[8] < 42 && i1840[8] > 0 && i1840[8] < i2[8] && i1840[8] + 1 > 0 →^* TRUE)∧(i1840[8] →^* i1840[9])∧(java.lang.Object(ARRAY(i2[8], a7588data[8])) →^* java.lang.Object(ARRAY(i2[9], a7588data[9])))∧(java.lang.Object(Tree(NULL, o8366[8], o8367[8])) →^* java.lang.Object(Tree(NULL, o8366[9], o8367[9])))∧(java.lang.Object(java.lang.String(i1942[8], i1941[8], i1943[8], a7876[8])) →^* java.lang.Object(java.lang.String(i1942[9], i1941[9], i1943[9], a7876[9]))))

(9) -> (0), if ((i1840[9] + 1 →^* i1876[0])∧(java.lang.Object(ARRAY(i2[9], a7588data[9])) →^* java.lang.Object(ARRAY(i2[0], a7588data[0])))∧(java.lang.Object(Tree(NULL, o8366[9], o8367[9])) →^* java.lang.Object(Tree(o8359[0], java.lang.Object(Tree(o8442Field0[0], o8442Field1[0], o8442Field2[0])), o8361[0]))))

The set Q consists of the following terms:
Load13105(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(x3, java.lang.Object(Tree(x4, x5, x6)), x7)))
Load12814(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(x3, java.lang.Object(Tree(x4, x5, x6)), x7)))
Load12814ARR1(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(NULL, java.lang.Object(Tree(x3, java.lang.Object(Tree(x4, x5, x6)), x7)), x7)), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
Cond_Load12814ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(NULL, java.lang.Object(Tree(x3, java.lang.Object(Tree(x4, x5, x6)), x7)), x7)), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
Load12814(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(java.lang.Object(Tree(x3, x4, x5)), x6, x7)))
Load12814ARR2(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x3, x4, x5)), x6, x7)), NULL, x7)), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
Cond_Load12814ARR2(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x3, x4, x5)), x6, x7)), NULL, x7)), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
Load12814(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(NULL, x3, x4)))
Load12814ARR3(java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(NULL, x3, x4)), java.lang.Object(java.lang.String(x5, x6, x7, x8)))
Cond_Load12814ARR3(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, java.lang.Object(Tree(NULL, x3, x4)), java.lang.Object(java.lang.String(x5, x6, x7, x8)))

(8) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(9) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD13105(java.lang.Object(ARRAY(i2[0], a7588data[0])), i1876[0], java.lang.Object(Tree(o8359[0], java.lang.Object(Tree(o8442Field0[0], o8442Field1[0], o8442Field2[0])), o8361[0]))) → LOAD12814(java.lang.Object(ARRAY(i2[0], a7588data[0])), i1876[0], java.lang.Object(Tree(o8442Field0[0], o8442Field1[0], o8442Field2[0])))
(1): LOAD12814(java.lang.Object(ARRAY(i2[1], a7588data[1])), i1840[1], java.lang.Object(Tree(o8359[1], java.lang.Object(Tree(o8442Field0[1], o8442Field1[1], o8442Field2[1])), o8361[1]))) → LOAD12814ARR1(java.lang.Object(ARRAY(i2[1], a7588data[1])), i1840[1], java.lang.Object(Tree(o8359[1], java.lang.Object(Tree(o8442Field0[1], o8442Field1[1], o8442Field2[1])), o8361[1])), java.lang.Object(java.lang.String(i1942[1], i1941[1], i1943[1], a7876[1])))
(2): LOAD12814ARR1(java.lang.Object(ARRAY(i2[2], a7588data[2])), i1840[2], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[2], java.lang.Object(Tree(o8442Field0[2], o8442Field1[2], o8442Field2[2])), o8361[2])), o8361[2])), java.lang.Object(java.lang.String(i1942[2], i1941[2], i1943[2], a7876[2]))) → COND_LOAD12814ARR1(i1942[2] >= 42 && i1840[2] > 0 && i1840[2] < i2[2] && i1840[2] + 1 > 0, java.lang.Object(ARRAY(i2[2], a7588data[2])), i1840[2], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[2], java.lang.Object(Tree(o8442Field0[2], o8442Field1[2], o8442Field2[2])), o8361[2])), o8361[2])), java.lang.Object(java.lang.String(i1942[2], i1941[2], i1943[2], a7876[2])))
(3): COND_LOAD12814ARR1(TRUE, java.lang.Object(ARRAY(i2[3], a7588data[3])), i1840[3], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[3], java.lang.Object(Tree(o8442Field0[3], o8442Field1[3], o8442Field2[3])), o8361[3])), o8361[3])), java.lang.Object(java.lang.String(i1942[3], i1941[3], i1943[3], a7876[3]))) → LOAD12814(java.lang.Object(ARRAY(i2[3], a7588data[3])), i1840[3] + 1, java.lang.Object(Tree(o8442Field0[3], o8442Field1[3], o8442Field2[3])))
(4): LOAD12814(java.lang.Object(ARRAY(i2[4], a7588data[4])), i1840[4], java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[4], o8443Field1[4], o8443Field2[4])), o8366[4], o8367[4]))) → LOAD12814ARR2(java.lang.Object(ARRAY(i2[4], a7588data[4])), i1840[4], java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[4], o8443Field1[4], o8443Field2[4])), o8366[4], o8367[4])), java.lang.Object(java.lang.String(i1942[4], i1941[4], i1943[4], a7876[4])))
(5): LOAD12814ARR2(java.lang.Object(ARRAY(i2[5], a7588data[5])), i1840[5], java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[5], o8443Field1[5], o8443Field2[5])), o8366[5], o8367[5])), NULL, o8367[5])), java.lang.Object(java.lang.String(i1942[5], i1941[5], i1943[5], a7876[5]))) → COND_LOAD12814ARR2(i1942[5] >= 0 && i1942[5] < 42 && i1840[5] > 0 && i1840[5] < i2[5] && i1840[5] + 1 > 0, java.lang.Object(ARRAY(i2[5], a7588data[5])), i1840[5], java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[5], o8443Field1[5], o8443Field2[5])), o8366[5], o8367[5])), NULL, o8367[5])), java.lang.Object(java.lang.String(i1942[5], i1941[5], i1943[5], a7876[5])))
(6): COND_LOAD12814ARR2(TRUE, java.lang.Object(ARRAY(i2[6], a7588data[6])), i1840[6], java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[6], o8443Field1[6], o8443Field2[6])), o8366[6], o8367[6])), NULL, o8367[6])), java.lang.Object(java.lang.String(i1942[6], i1941[6], i1943[6], a7876[6]))) → LOAD12814(java.lang.Object(ARRAY(i2[6], a7588data[6])), i1840[6] + 1, java.lang.Object(Tree(o8443Field0[6], o8443Field1[6], o8443Field2[6])))
(7): LOAD12814(java.lang.Object(ARRAY(i2[7], a7588data[7])), i1840[7], java.lang.Object(Tree(NULL, o8366[7], o8367[7]))) → LOAD12814ARR3(java.lang.Object(ARRAY(i2[7], a7588data[7])), i1840[7], java.lang.Object(Tree(NULL, o8366[7], o8367[7])), java.lang.Object(java.lang.String(i1942[7], i1941[7], i1943[7], a7876[7])))
(8): LOAD12814ARR3(java.lang.Object(ARRAY(i2[8], a7588data[8])), i1840[8], java.lang.Object(Tree(NULL, o8366[8], o8367[8])), java.lang.Object(java.lang.String(i1942[8], i1941[8], i1943[8], a7876[8]))) → COND_LOAD12814ARR3(i1942[8] >= 0 && i1942[8] < 42 && i1840[8] > 0 && i1840[8] < i2[8] && i1840[8] + 1 > 0, java.lang.Object(ARRAY(i2[8], a7588data[8])), i1840[8], java.lang.Object(Tree(NULL, o8366[8], o8367[8])), java.lang.Object(java.lang.String(i1942[8], i1941[8], i1943[8], a7876[8])))
(9): COND_LOAD12814ARR3(TRUE, java.lang.Object(ARRAY(i2[9], a7588data[9])), i1840[9], java.lang.Object(Tree(NULL, o8366[9], o8367[9])), java.lang.Object(java.lang.String(i1942[9], i1941[9], i1943[9], a7876[9]))) → LOAD13105(java.lang.Object(ARRAY(i2[9], a7588data[9])), i1840[9] + 1, java.lang.Object(Tree(NULL, o8366[9], o8367[9])))

(10) ItpfGraphProof (EQUIVALENT transformation)

Applied rule ItpfICap [ICap]

(11) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

(0) -> (1), if (((i2[0] →^* i2[1])∧(a7588data[0] →^* a7588data[1]))∧(i1876[0] →^* i1840[1])∧((o8442Field0[0] →^* o8359[1])∧(o8442Field1[0] →^* java.lang.Object(Tree(o8442Field0[1], o8442Field1[1], o8442Field2[1])))∧(o8442Field2[0] →^* o8361[1])))

(0) -> (4), if ((i1876[0] →^* i1840[4])∧((o8442Field0[0] →^* java.lang.Object(Tree(o8443Field0[4], o8443Field1[4], o8443Field2[4])))∧(o8442Field1[0] →^* o8366[4])∧(o8442Field2[0] →^* o8367[4]))∧((i2[0] →^* i2[4])∧(a7588data[0] →^* a7588data[4])))

(0) -> (7), if (((i2[0] →^* i2[7])∧(a7588data[0] →^* a7588data[7]))∧(i1876[0] →^* i1840[7])∧((o8442Field0[0] →^* NULL)∧(o8442Field1[0] →^* o8366[7])∧(o8442Field2[0] →^* o8367[7])))

(1) -> (2), if (((i1942[1] →^* i1942[2])∧(i1941[1] →^* i1941[2])∧(i1943[1] →^* i1943[2])∧(a7876[1] →^* a7876[2]))∧((i2[1] →^* i2[2])∧(a7588data[1] →^* a7588data[2]))∧((o8359[1] →^* NULL)∧(o8442Field0[1] →^* o8359[2])∧(o8442Field1[1] →^* java.lang.Object(Tree(o8442Field0[2], o8442Field1[2], o8442Field2[2])))∧(o8442Field2[1] →^* o8361[2])∧(o8361[1] →^* o8361[2]))∧(i1840[1] →^* i1840[2]))

(2) -> (3), if (((o8359[2] →^* o8359[3])∧(o8442Field0[2] →^* o8442Field0[3])∧(o8442Field1[2] →^* o8442Field1[3])∧(o8442Field2[2] →^* o8442Field2[3])∧(o8361[2] →^* o8361[3]))∧(i1942[2] >= 42 && i1840[2] > 0 && i1840[2] < i2[2] && i1840[2] + 1 > 0 →^* TRUE)∧((i1942[2] →^* i1942[3])∧(i1941[2] →^* i1941[3])∧(i1943[2] →^* i1943[3])∧(a7876[2] →^* a7876[3]))∧(i1840[2] →^* i1840[3])∧((i2[2] →^* i2[3])∧(a7588data[2] →^* a7588data[3])))

(3) -> (1), if (((i2[3] →^* i2[1])∧(a7588data[3] →^* a7588data[1]))∧(i1840[3] + 1 →^* i1840[1])∧((o8442Field0[3] →^* o8359[1])∧(o8442Field1[3] →^* java.lang.Object(Tree(o8442Field0[1], o8442Field1[1], o8442Field2[1])))∧(o8442Field2[3] →^* o8361[1])))

(3) -> (4), if (((o8442Field0[3] →^* java.lang.Object(Tree(o8443Field0[4], o8443Field1[4], o8443Field2[4])))∧(o8442Field1[3] →^* o8366[4])∧(o8442Field2[3] →^* o8367[4]))∧(i1840[3] + 1 →^* i1840[4])∧((i2[3] →^* i2[4])∧(a7588data[3] →^* a7588data[4])))

(3) -> (7), if ((i1840[3] + 1 →^* i1840[7])∧((o8442Field0[3] →^* NULL)∧(o8442Field1[3] →^* o8366[7])∧(o8442Field2[3] →^* o8367[7]))∧((i2[3] →^* i2[7])∧(a7588data[3] →^* a7588data[7])))

(4) -> (5), if (((o8443Field0[4] →^* java.lang.Object(Tree(o8443Field0[5], o8443Field1[5], o8443Field2[5])))∧(o8443Field1[4] →^* o8366[5])∧(o8443Field2[4] →^* o8367[5])∧(o8366[4] →^* NULL)∧(o8367[4] →^* o8367[5]))∧(i1840[4] →^* i1840[5])∧((i1942[4] →^* i1942[5])∧(i1941[4] →^* i1941[5])∧(i1943[4] →^* i1943[5])∧(a7876[4] →^* a7876[5]))∧((i2[4] →^* i2[5])∧(a7588data[4] →^* a7588data[5])))

(5) -> (6), if (((i1942[5] →^* i1942[6])∧(i1941[5] →^* i1941[6])∧(i1943[5] →^* i1943[6])∧(a7876[5] →^* a7876[6]))∧((o8443Field0[5] →^* o8443Field0[6])∧(o8443Field1[5] →^* o8443Field1[6])∧(o8443Field2[5] →^* o8443Field2[6])∧(o8366[5] →^* o8366[6])∧(o8367[5] →^* o8367[6]))∧(i1840[5] →^* i1840[6])∧((i2[5] →^* i2[6])∧(a7588data[5] →^* a7588data[6]))∧(i1942[5] >= 0 && i1942[5] < 42 && i1840[5] > 0 && i1840[5] < i2[5] && i1840[5] + 1 > 0 →^* TRUE))

(6) -> (1), if ((i1840[6] + 1 →^* i1840[1])∧((i2[6] →^* i2[1])∧(a7588data[6] →^* a7588data[1]))∧((o8443Field0[6] →^* o8359[1])∧(o8443Field1[6] →^* java.lang.Object(Tree(o8442Field0[1], o8442Field1[1], o8442Field2[1])))∧(o8443Field2[6] →^* o8361[1])))

(6) -> (4), if (((i2[6] →^* i2[4])∧(a7588data[6] →^* a7588data[4]))∧(i1840[6] + 1 →^* i1840[4])∧((o8443Field0[6] →^* java.lang.Object(Tree(o8443Field0[4], o8443Field1[4], o8443Field2[4])))∧(o8443Field1[6] →^* o8366[4])∧(o8443Field2[6] →^* o8367[4])))

(6) -> (7), if (((i2[6] →^* i2[7])∧(a7588data[6] →^* a7588data[7]))∧((o8443Field0[6] →^* NULL)∧(o8443Field1[6] →^* o8366[7])∧(o8443Field2[6] →^* o8367[7]))∧(i1840[6] + 1 →^* i1840[7]))

(7) -> (8), if (((i1942[7] →^* i1942[8])∧(i1941[7] →^* i1941[8])∧(i1943[7] →^* i1943[8])∧(a7876[7] →^* a7876[8]))∧(i1840[7] →^* i1840[8])∧((i2[7] →^* i2[8])∧(a7588data[7] →^* a7588data[8]))∧((o8366[7] →^* o8366[8])∧(o8367[7] →^* o8367[8])))

(8) -> (9), if ((i1942[8] >= 0 && i1942[8] < 42 && i1840[8] > 0 && i1840[8] < i2[8] && i1840[8] + 1 > 0 →^* TRUE)∧(i1840[8] →^* i1840[9])∧((i2[8] →^* i2[9])∧(a7588data[8] →^* a7588data[9]))∧((o8366[8] →^* o8366[9])∧(o8367[8] →^* o8367[9]))∧((i1942[8] →^* i1942[9])∧(i1941[8] →^* i1941[9])∧(i1943[8] →^* i1943[9])∧(a7876[8] →^* a7876[9])))

(9) -> (0), if ((i1840[9] + 1 →^* i1876[0])∧((i2[9] →^* i2[0])∧(a7588data[9] →^* a7588data[0]))∧((o8366[9] →^* java.lang.Object(Tree(o8442Field0[0], o8442Field1[0], o8442Field2[0])))∧(o8367[9] →^* o8361[0])))

(12) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair LOAD13105(java.lang.Object(ARRAY(i2, a7588data)), i1876, java.lang.Object(Tree(o8359, java.lang.Object(Tree(o8442Field0, o8442Field1, o8442Field2)), o8361))) → LOAD12814(java.lang.Object(ARRAY(i2, a7588data)), i1876, java.lang.Object(Tree(o8442Field0, o8442Field1, o8442Field2))) the following chains were created:

We consider the chain LOAD13105(java.lang.Object(ARRAY(i2[0], a7588data[0])), i1876[0], java.lang.Object(Tree(o8359[0], java.lang.Object(Tree(o8442Field0[0], o8442Field1[0], o8442Field2[0])), o8361[0]))) → LOAD12814(java.lang.Object(ARRAY(i2[0], a7588data[0])), i1876[0], java.lang.Object(Tree(o8442Field0[0], o8442Field1[0], o8442Field2[0]))) which results in the following constraint:
(1)    (LOAD13105(java.lang.Object(ARRAY(i2[0], a7588data[0])), i1876[0], java.lang.Object(Tree(o8359[0], java.lang.Object(Tree(o8442Field0[0], o8442Field1[0], o8442Field2[0])), o8361[0])))≥NonInfC∧LOAD13105(java.lang.Object(ARRAY(i2[0], a7588data[0])), i1876[0], java.lang.Object(Tree(o8359[0], java.lang.Object(Tree(o8442Field0[0], o8442Field1[0], o8442Field2[0])), o8361[0])))≥LOAD12814(java.lang.Object(ARRAY(i2[0], a7588data[0])), i1876[0], java.lang.Object(Tree(o8442Field0[0], o8442Field1[0], o8442Field2[0])))∧(U^Increasing(LOAD12814(java.lang.Object(ARRAY(i2[0], a7588data[0])), i1876[0], java.lang.Object(Tree(o8442Field0[0], o8442Field1[0], o8442Field2[0])))), ≥))

We simplified constraint (1) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(2)    ((U^Increasing(LOAD12814(java.lang.Object(ARRAY(i2[0], a7588data[0])), i1876[0], java.lang.Object(Tree(o8442Field0[0], o8442Field1[0], o8442Field2[0])))), ≥)∧[(-1)bso_31] ≥ 0)

We simplified constraint (2) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(3)    ((U^Increasing(LOAD12814(java.lang.Object(ARRAY(i2[0], a7588data[0])), i1876[0], java.lang.Object(Tree(o8442Field0[0], o8442Field1[0], o8442Field2[0])))), ≥)∧[(-1)bso_31] ≥ 0)

We simplified constraint (3) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(4)    ((U^Increasing(LOAD12814(java.lang.Object(ARRAY(i2[0], a7588data[0])), i1876[0], java.lang.Object(Tree(o8442Field0[0], o8442Field1[0], o8442Field2[0])))), ≥)∧[(-1)bso_31] ≥ 0)

We simplified constraint (4) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(5)    ((U^Increasing(LOAD12814(java.lang.Object(ARRAY(i2[0], a7588data[0])), i1876[0], java.lang.Object(Tree(o8442Field0[0], o8442Field1[0], o8442Field2[0])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_31] ≥ 0)

For Pair LOAD12814(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(o8359, java.lang.Object(Tree(o8442Field0, o8442Field1, o8442Field2)), o8361))) → LOAD12814ARR1(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(o8359, java.lang.Object(Tree(o8442Field0, o8442Field1, o8442Field2)), o8361)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876))) the following chains were created:

We consider the chain LOAD12814(java.lang.Object(ARRAY(i2[1], a7588data[1])), i1840[1], java.lang.Object(Tree(o8359[1], java.lang.Object(Tree(o8442Field0[1], o8442Field1[1], o8442Field2[1])), o8361[1]))) → LOAD12814ARR1(java.lang.Object(ARRAY(i2[1], a7588data[1])), i1840[1], java.lang.Object(Tree(o8359[1], java.lang.Object(Tree(o8442Field0[1], o8442Field1[1], o8442Field2[1])), o8361[1])), java.lang.Object(java.lang.String(i1942[1], i1941[1], i1943[1], a7876[1]))) which results in the following constraint:
(6)    (LOAD12814(java.lang.Object(ARRAY(i2[1], a7588data[1])), i1840[1], java.lang.Object(Tree(o8359[1], java.lang.Object(Tree(o8442Field0[1], o8442Field1[1], o8442Field2[1])), o8361[1])))≥NonInfC∧LOAD12814(java.lang.Object(ARRAY(i2[1], a7588data[1])), i1840[1], java.lang.Object(Tree(o8359[1], java.lang.Object(Tree(o8442Field0[1], o8442Field1[1], o8442Field2[1])), o8361[1])))≥LOAD12814ARR1(java.lang.Object(ARRAY(i2[1], a7588data[1])), i1840[1], java.lang.Object(Tree(o8359[1], java.lang.Object(Tree(o8442Field0[1], o8442Field1[1], o8442Field2[1])), o8361[1])), java.lang.Object(java.lang.String(i1942[1], i1941[1], i1943[1], a7876[1])))∧(U^Increasing(LOAD12814ARR1(java.lang.Object(ARRAY(i2[1], a7588data[1])), i1840[1], java.lang.Object(Tree(o8359[1], java.lang.Object(Tree(o8442Field0[1], o8442Field1[1], o8442Field2[1])), o8361[1])), java.lang.Object(java.lang.String(i1942[1], i1941[1], i1943[1], a7876[1])))), ≥))

We simplified constraint (6) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(7)    ((U^Increasing(LOAD12814ARR1(java.lang.Object(ARRAY(i2[1], a7588data[1])), i1840[1], java.lang.Object(Tree(o8359[1], java.lang.Object(Tree(o8442Field0[1], o8442Field1[1], o8442Field2[1])), o8361[1])), java.lang.Object(java.lang.String(i1942[1], i1941[1], i1943[1], a7876[1])))), ≥)∧[1 + (-1)bso_33] ≥ 0)

We simplified constraint (7) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(8)    ((U^Increasing(LOAD12814ARR1(java.lang.Object(ARRAY(i2[1], a7588data[1])), i1840[1], java.lang.Object(Tree(o8359[1], java.lang.Object(Tree(o8442Field0[1], o8442Field1[1], o8442Field2[1])), o8361[1])), java.lang.Object(java.lang.String(i1942[1], i1941[1], i1943[1], a7876[1])))), ≥)∧[1 + (-1)bso_33] ≥ 0)

We simplified constraint (8) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(9)    ((U^Increasing(LOAD12814ARR1(java.lang.Object(ARRAY(i2[1], a7588data[1])), i1840[1], java.lang.Object(Tree(o8359[1], java.lang.Object(Tree(o8442Field0[1], o8442Field1[1], o8442Field2[1])), o8361[1])), java.lang.Object(java.lang.String(i1942[1], i1941[1], i1943[1], a7876[1])))), ≥)∧[1 + (-1)bso_33] ≥ 0)

We simplified constraint (9) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(10)    ((U^Increasing(LOAD12814ARR1(java.lang.Object(ARRAY(i2[1], a7588data[1])), i1840[1], java.lang.Object(Tree(o8359[1], java.lang.Object(Tree(o8442Field0[1], o8442Field1[1], o8442Field2[1])), o8361[1])), java.lang.Object(java.lang.String(i1942[1], i1941[1], i1943[1], a7876[1])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_33] ≥ 0)

For Pair LOAD12814ARR1(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359, java.lang.Object(Tree(o8442Field0, o8442Field1, o8442Field2)), o8361)), o8361)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876))) → COND_LOAD12814ARR1(&&(&&(&&(>=(i1942, 42), >(i1840, 0)), <(i1840, i2)), >(+(i1840, 1), 0)), java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359, java.lang.Object(Tree(o8442Field0, o8442Field1, o8442Field2)), o8361)), o8361)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876))) the following chains were created:

We consider the chain LOAD12814ARR1(java.lang.Object(ARRAY(i2[2], a7588data[2])), i1840[2], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[2], java.lang.Object(Tree(o8442Field0[2], o8442Field1[2], o8442Field2[2])), o8361[2])), o8361[2])), java.lang.Object(java.lang.String(i1942[2], i1941[2], i1943[2], a7876[2]))) → COND_LOAD12814ARR1(&&(&&(&&(>=(i1942[2], 42), >(i1840[2], 0)), <(i1840[2], i2[2])), >(+(i1840[2], 1), 0)), java.lang.Object(ARRAY(i2[2], a7588data[2])), i1840[2], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[2], java.lang.Object(Tree(o8442Field0[2], o8442Field1[2], o8442Field2[2])), o8361[2])), o8361[2])), java.lang.Object(java.lang.String(i1942[2], i1941[2], i1943[2], a7876[2]))), COND_LOAD12814ARR1(TRUE, java.lang.Object(ARRAY(i2[3], a7588data[3])), i1840[3], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[3], java.lang.Object(Tree(o8442Field0[3], o8442Field1[3], o8442Field2[3])), o8361[3])), o8361[3])), java.lang.Object(java.lang.String(i1942[3], i1941[3], i1943[3], a7876[3]))) → LOAD12814(java.lang.Object(ARRAY(i2[3], a7588data[3])), +(i1840[3], 1), java.lang.Object(Tree(o8442Field0[3], o8442Field1[3], o8442Field2[3]))) which results in the following constraint:
(11)    (o8359[2]=o8359[3]∧o8442Field0[2]=o8442Field0[3]∧o8442Field1[2]=o8442Field1[3]∧o8442Field2[2]=o8442Field2[3]∧o8361[2]=o8361[3]∧&&(&&(&&(>=(i1942[2], 42), >(i1840[2], 0)), <(i1840[2], i2[2])), >(+(i1840[2], 1), 0))=TRUE∧i1942[2]=i1942[3]∧i1941[2]=i1941[3]∧i1943[2]=i1943[3]∧a7876[2]=a7876[3]∧i1840[2]=i1840[3]∧i2[2]=i2[3]∧a7588data[2]=a7588data[3] ⇒ LOAD12814ARR1(java.lang.Object(ARRAY(i2[2], a7588data[2])), i1840[2], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[2], java.lang.Object(Tree(o8442Field0[2], o8442Field1[2], o8442Field2[2])), o8361[2])), o8361[2])), java.lang.Object(java.lang.String(i1942[2], i1941[2], i1943[2], a7876[2])))≥NonInfC∧LOAD12814ARR1(java.lang.Object(ARRAY(i2[2], a7588data[2])), i1840[2], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[2], java.lang.Object(Tree(o8442Field0[2], o8442Field1[2], o8442Field2[2])), o8361[2])), o8361[2])), java.lang.Object(java.lang.String(i1942[2], i1941[2], i1943[2], a7876[2])))≥COND_LOAD12814ARR1(&&(&&(&&(>=(i1942[2], 42), >(i1840[2], 0)), <(i1840[2], i2[2])), >(+(i1840[2], 1), 0)), java.lang.Object(ARRAY(i2[2], a7588data[2])), i1840[2], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[2], java.lang.Object(Tree(o8442Field0[2], o8442Field1[2], o8442Field2[2])), o8361[2])), o8361[2])), java.lang.Object(java.lang.String(i1942[2], i1941[2], i1943[2], a7876[2])))∧(U^Increasing(COND_LOAD12814ARR1(&&(&&(&&(>=(i1942[2], 42), >(i1840[2], 0)), <(i1840[2], i2[2])), >(+(i1840[2], 1), 0)), java.lang.Object(ARRAY(i2[2], a7588data[2])), i1840[2], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[2], java.lang.Object(Tree(o8442Field0[2], o8442Field1[2], o8442Field2[2])), o8361[2])), o8361[2])), java.lang.Object(java.lang.String(i1942[2], i1941[2], i1943[2], a7876[2])))), ≥))

We simplified constraint (11) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:
(12)    (>(+(i1840[2], 1), 0)=TRUE∧<(i1840[2], i2[2])=TRUE∧>=(i1942[2], 42)=TRUE∧>(i1840[2], 0)=TRUE ⇒ LOAD12814ARR1(java.lang.Object(ARRAY(i2[2], a7588data[2])), i1840[2], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[2], java.lang.Object(Tree(o8442Field0[2], o8442Field1[2], o8442Field2[2])), o8361[2])), o8361[2])), java.lang.Object(java.lang.String(i1942[2], i1941[2], i1943[2], a7876[2])))≥NonInfC∧LOAD12814ARR1(java.lang.Object(ARRAY(i2[2], a7588data[2])), i1840[2], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[2], java.lang.Object(Tree(o8442Field0[2], o8442Field1[2], o8442Field2[2])), o8361[2])), o8361[2])), java.lang.Object(java.lang.String(i1942[2], i1941[2], i1943[2], a7876[2])))≥COND_LOAD12814ARR1(&&(&&(&&(>=(i1942[2], 42), >(i1840[2], 0)), <(i1840[2], i2[2])), >(+(i1840[2], 1), 0)), java.lang.Object(ARRAY(i2[2], a7588data[2])), i1840[2], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[2], java.lang.Object(Tree(o8442Field0[2], o8442Field1[2], o8442Field2[2])), o8361[2])), o8361[2])), java.lang.Object(java.lang.String(i1942[2], i1941[2], i1943[2], a7876[2])))∧(U^Increasing(COND_LOAD12814ARR1(&&(&&(&&(>=(i1942[2], 42), >(i1840[2], 0)), <(i1840[2], i2[2])), >(+(i1840[2], 1), 0)), java.lang.Object(ARRAY(i2[2], a7588data[2])), i1840[2], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[2], java.lang.Object(Tree(o8442Field0[2], o8442Field1[2], o8442Field2[2])), o8361[2])), o8361[2])), java.lang.Object(java.lang.String(i1942[2], i1941[2], i1943[2], a7876[2])))), ≥))

We simplified constraint (12) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(13)    (i1840[2] ≥ 0∧i2[2] + [-1] + [-1]i1840[2] ≥ 0∧i1942[2] + [-42] ≥ 0∧i1840[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_LOAD12814ARR1(&&(&&(&&(>=(i1942[2], 42), >(i1840[2], 0)), <(i1840[2], i2[2])), >(+(i1840[2], 1), 0)), java.lang.Object(ARRAY(i2[2], a7588data[2])), i1840[2], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[2], java.lang.Object(Tree(o8442Field0[2], o8442Field1[2], o8442Field2[2])), o8361[2])), o8361[2])), java.lang.Object(java.lang.String(i1942[2], i1941[2], i1943[2], a7876[2])))), ≥)∧[bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]i1840[2] + [bni_34]i2[2] ≥ 0∧[(-1)bso_35] ≥ 0)

We simplified constraint (13) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(14)    (i1840[2] ≥ 0∧i2[2] + [-1] + [-1]i1840[2] ≥ 0∧i1942[2] + [-42] ≥ 0∧i1840[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_LOAD12814ARR1(&&(&&(&&(>=(i1942[2], 42), >(i1840[2], 0)), <(i1840[2], i2[2])), >(+(i1840[2], 1), 0)), java.lang.Object(ARRAY(i2[2], a7588data[2])), i1840[2], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[2], java.lang.Object(Tree(o8442Field0[2], o8442Field1[2], o8442Field2[2])), o8361[2])), o8361[2])), java.lang.Object(java.lang.String(i1942[2], i1941[2], i1943[2], a7876[2])))), ≥)∧[bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]i1840[2] + [bni_34]i2[2] ≥ 0∧[(-1)bso_35] ≥ 0)

We simplified constraint (14) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(15)    (i1840[2] ≥ 0∧i2[2] + [-1] + [-1]i1840[2] ≥ 0∧i1942[2] + [-42] ≥ 0∧i1840[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_LOAD12814ARR1(&&(&&(&&(>=(i1942[2], 42), >(i1840[2], 0)), <(i1840[2], i2[2])), >(+(i1840[2], 1), 0)), java.lang.Object(ARRAY(i2[2], a7588data[2])), i1840[2], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[2], java.lang.Object(Tree(o8442Field0[2], o8442Field1[2], o8442Field2[2])), o8361[2])), o8361[2])), java.lang.Object(java.lang.String(i1942[2], i1941[2], i1943[2], a7876[2])))), ≥)∧[bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]i1840[2] + [bni_34]i2[2] ≥ 0∧[(-1)bso_35] ≥ 0)

We simplified constraint (15) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(16)    (i1840[2] ≥ 0∧i2[2] + [-1] + [-1]i1840[2] ≥ 0∧i1942[2] + [-42] ≥ 0∧i1840[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_LOAD12814ARR1(&&(&&(&&(>=(i1942[2], 42), >(i1840[2], 0)), <(i1840[2], i2[2])), >(+(i1840[2], 1), 0)), java.lang.Object(ARRAY(i2[2], a7588data[2])), i1840[2], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[2], java.lang.Object(Tree(o8442Field0[2], o8442Field1[2], o8442Field2[2])), o8361[2])), o8361[2])), java.lang.Object(java.lang.String(i1942[2], i1941[2], i1943[2], a7876[2])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]i1840[2] + [bni_34]i2[2] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)

We simplified constraint (16) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(17)    ([1] + i1840[2] ≥ 0∧i2[2] + [-2] + [-1]i1840[2] ≥ 0∧i1942[2] + [-42] ≥ 0∧i1840[2] ≥ 0 ⇒ (U^Increasing(COND_LOAD12814ARR1(&&(&&(&&(>=(i1942[2], 42), >(i1840[2], 0)), <(i1840[2], i2[2])), >(+(i1840[2], 1), 0)), java.lang.Object(ARRAY(i2[2], a7588data[2])), i1840[2], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[2], java.lang.Object(Tree(o8442Field0[2], o8442Field1[2], o8442Field2[2])), o8361[2])), o8361[2])), java.lang.Object(java.lang.String(i1942[2], i1941[2], i1943[2], a7876[2])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)Bound*bni_34] + [(-1)bni_34]i1840[2] + [bni_34]i2[2] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)

We simplified constraint (17) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(18)    ([1] + i1840[2] ≥ 0∧i2[2] ≥ 0∧i1942[2] + [-42] ≥ 0∧i1840[2] ≥ 0 ⇒ (U^Increasing(COND_LOAD12814ARR1(&&(&&(&&(>=(i1942[2], 42), >(i1840[2], 0)), <(i1840[2], i2[2])), >(+(i1840[2], 1), 0)), java.lang.Object(ARRAY(i2[2], a7588data[2])), i1840[2], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[2], java.lang.Object(Tree(o8442Field0[2], o8442Field1[2], o8442Field2[2])), o8361[2])), o8361[2])), java.lang.Object(java.lang.String(i1942[2], i1941[2], i1943[2], a7876[2])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)Bound*bni_34 + (2)bni_34] + [bni_34]i2[2] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)

We simplified constraint (18) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(19)    ([1] + i1840[2] ≥ 0∧i2[2] ≥ 0∧i1942[2] ≥ 0∧i1840[2] ≥ 0 ⇒ (U^Increasing(COND_LOAD12814ARR1(&&(&&(&&(>=(i1942[2], 42), >(i1840[2], 0)), <(i1840[2], i2[2])), >(+(i1840[2], 1), 0)), java.lang.Object(ARRAY(i2[2], a7588data[2])), i1840[2], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[2], java.lang.Object(Tree(o8442Field0[2], o8442Field1[2], o8442Field2[2])), o8361[2])), o8361[2])), java.lang.Object(java.lang.String(i1942[2], i1941[2], i1943[2], a7876[2])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)Bound*bni_34 + (2)bni_34] + [bni_34]i2[2] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)

For Pair COND_LOAD12814ARR1(TRUE, java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359, java.lang.Object(Tree(o8442Field0, o8442Field1, o8442Field2)), o8361)), o8361)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876))) → LOAD12814(java.lang.Object(ARRAY(i2, a7588data)), +(i1840, 1), java.lang.Object(Tree(o8442Field0, o8442Field1, o8442Field2))) the following chains were created:

We consider the chain COND_LOAD12814ARR1(TRUE, java.lang.Object(ARRAY(i2[3], a7588data[3])), i1840[3], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[3], java.lang.Object(Tree(o8442Field0[3], o8442Field1[3], o8442Field2[3])), o8361[3])), o8361[3])), java.lang.Object(java.lang.String(i1942[3], i1941[3], i1943[3], a7876[3]))) → LOAD12814(java.lang.Object(ARRAY(i2[3], a7588data[3])), +(i1840[3], 1), java.lang.Object(Tree(o8442Field0[3], o8442Field1[3], o8442Field2[3]))) which results in the following constraint:
(20)    (COND_LOAD12814ARR1(TRUE, java.lang.Object(ARRAY(i2[3], a7588data[3])), i1840[3], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[3], java.lang.Object(Tree(o8442Field0[3], o8442Field1[3], o8442Field2[3])), o8361[3])), o8361[3])), java.lang.Object(java.lang.String(i1942[3], i1941[3], i1943[3], a7876[3])))≥NonInfC∧COND_LOAD12814ARR1(TRUE, java.lang.Object(ARRAY(i2[3], a7588data[3])), i1840[3], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[3], java.lang.Object(Tree(o8442Field0[3], o8442Field1[3], o8442Field2[3])), o8361[3])), o8361[3])), java.lang.Object(java.lang.String(i1942[3], i1941[3], i1943[3], a7876[3])))≥LOAD12814(java.lang.Object(ARRAY(i2[3], a7588data[3])), +(i1840[3], 1), java.lang.Object(Tree(o8442Field0[3], o8442Field1[3], o8442Field2[3])))∧(U^Increasing(LOAD12814(java.lang.Object(ARRAY(i2[3], a7588data[3])), +(i1840[3], 1), java.lang.Object(Tree(o8442Field0[3], o8442Field1[3], o8442Field2[3])))), ≥))

We simplified constraint (20) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(21)    ((U^Increasing(LOAD12814(java.lang.Object(ARRAY(i2[3], a7588data[3])), +(i1840[3], 1), java.lang.Object(Tree(o8442Field0[3], o8442Field1[3], o8442Field2[3])))), ≥)∧[(-1)bso_37] ≥ 0)

We simplified constraint (21) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(22)    ((U^Increasing(LOAD12814(java.lang.Object(ARRAY(i2[3], a7588data[3])), +(i1840[3], 1), java.lang.Object(Tree(o8442Field0[3], o8442Field1[3], o8442Field2[3])))), ≥)∧[(-1)bso_37] ≥ 0)

We simplified constraint (22) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(23)    ((U^Increasing(LOAD12814(java.lang.Object(ARRAY(i2[3], a7588data[3])), +(i1840[3], 1), java.lang.Object(Tree(o8442Field0[3], o8442Field1[3], o8442Field2[3])))), ≥)∧[(-1)bso_37] ≥ 0)

We simplified constraint (23) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(24)    ((U^Increasing(LOAD12814(java.lang.Object(ARRAY(i2[3], a7588data[3])), +(i1840[3], 1), java.lang.Object(Tree(o8442Field0[3], o8442Field1[3], o8442Field2[3])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_37] ≥ 0)

For Pair LOAD12814(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0, o8443Field1, o8443Field2)), o8366, o8367))) → LOAD12814ARR2(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0, o8443Field1, o8443Field2)), o8366, o8367)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876))) the following chains were created:

We consider the chain LOAD12814(java.lang.Object(ARRAY(i2[4], a7588data[4])), i1840[4], java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[4], o8443Field1[4], o8443Field2[4])), o8366[4], o8367[4]))) → LOAD12814ARR2(java.lang.Object(ARRAY(i2[4], a7588data[4])), i1840[4], java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[4], o8443Field1[4], o8443Field2[4])), o8366[4], o8367[4])), java.lang.Object(java.lang.String(i1942[4], i1941[4], i1943[4], a7876[4]))) which results in the following constraint:
(25)    (LOAD12814(java.lang.Object(ARRAY(i2[4], a7588data[4])), i1840[4], java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[4], o8443Field1[4], o8443Field2[4])), o8366[4], o8367[4])))≥NonInfC∧LOAD12814(java.lang.Object(ARRAY(i2[4], a7588data[4])), i1840[4], java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[4], o8443Field1[4], o8443Field2[4])), o8366[4], o8367[4])))≥LOAD12814ARR2(java.lang.Object(ARRAY(i2[4], a7588data[4])), i1840[4], java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[4], o8443Field1[4], o8443Field2[4])), o8366[4], o8367[4])), java.lang.Object(java.lang.String(i1942[4], i1941[4], i1943[4], a7876[4])))∧(U^Increasing(LOAD12814ARR2(java.lang.Object(ARRAY(i2[4], a7588data[4])), i1840[4], java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[4], o8443Field1[4], o8443Field2[4])), o8366[4], o8367[4])), java.lang.Object(java.lang.String(i1942[4], i1941[4], i1943[4], a7876[4])))), ≥))

We simplified constraint (25) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(26)    ((U^Increasing(LOAD12814ARR2(java.lang.Object(ARRAY(i2[4], a7588data[4])), i1840[4], java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[4], o8443Field1[4], o8443Field2[4])), o8366[4], o8367[4])), java.lang.Object(java.lang.String(i1942[4], i1941[4], i1943[4], a7876[4])))), ≥)∧[(-1)bso_39] ≥ 0)

We simplified constraint (26) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(27)    ((U^Increasing(LOAD12814ARR2(java.lang.Object(ARRAY(i2[4], a7588data[4])), i1840[4], java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[4], o8443Field1[4], o8443Field2[4])), o8366[4], o8367[4])), java.lang.Object(java.lang.String(i1942[4], i1941[4], i1943[4], a7876[4])))), ≥)∧[(-1)bso_39] ≥ 0)

We simplified constraint (27) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(28)    ((U^Increasing(LOAD12814ARR2(java.lang.Object(ARRAY(i2[4], a7588data[4])), i1840[4], java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[4], o8443Field1[4], o8443Field2[4])), o8366[4], o8367[4])), java.lang.Object(java.lang.String(i1942[4], i1941[4], i1943[4], a7876[4])))), ≥)∧[(-1)bso_39] ≥ 0)

We simplified constraint (28) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(29)    ((U^Increasing(LOAD12814ARR2(java.lang.Object(ARRAY(i2[4], a7588data[4])), i1840[4], java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[4], o8443Field1[4], o8443Field2[4])), o8366[4], o8367[4])), java.lang.Object(java.lang.String(i1942[4], i1941[4], i1943[4], a7876[4])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_39] ≥ 0)

For Pair LOAD12814ARR2(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0, o8443Field1, o8443Field2)), o8366, o8367)), NULL, o8367)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876))) → COND_LOAD12814ARR2(&&(&&(&&(&&(>=(i1942, 0), <(i1942, 42)), >(i1840, 0)), <(i1840, i2)), >(+(i1840, 1), 0)), java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0, o8443Field1, o8443Field2)), o8366, o8367)), NULL, o8367)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876))) the following chains were created:

We consider the chain LOAD12814ARR2(java.lang.Object(ARRAY(i2[5], a7588data[5])), i1840[5], java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[5], o8443Field1[5], o8443Field2[5])), o8366[5], o8367[5])), NULL, o8367[5])), java.lang.Object(java.lang.String(i1942[5], i1941[5], i1943[5], a7876[5]))) → COND_LOAD12814ARR2(&&(&&(&&(&&(>=(i1942[5], 0), <(i1942[5], 42)), >(i1840[5], 0)), <(i1840[5], i2[5])), >(+(i1840[5], 1), 0)), java.lang.Object(ARRAY(i2[5], a7588data[5])), i1840[5], java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[5], o8443Field1[5], o8443Field2[5])), o8366[5], o8367[5])), NULL, o8367[5])), java.lang.Object(java.lang.String(i1942[5], i1941[5], i1943[5], a7876[5]))), COND_LOAD12814ARR2(TRUE, java.lang.Object(ARRAY(i2[6], a7588data[6])), i1840[6], java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[6], o8443Field1[6], o8443Field2[6])), o8366[6], o8367[6])), NULL, o8367[6])), java.lang.Object(java.lang.String(i1942[6], i1941[6], i1943[6], a7876[6]))) → LOAD12814(java.lang.Object(ARRAY(i2[6], a7588data[6])), +(i1840[6], 1), java.lang.Object(Tree(o8443Field0[6], o8443Field1[6], o8443Field2[6]))) which results in the following constraint:
(30)    (i1942[5]=i1942[6]∧i1941[5]=i1941[6]∧i1943[5]=i1943[6]∧a7876[5]=a7876[6]∧o8443Field0[5]=o8443Field0[6]∧o8443Field1[5]=o8443Field1[6]∧o8443Field2[5]=o8443Field2[6]∧o8366[5]=o8366[6]∧o8367[5]=o8367[6]∧i1840[5]=i1840[6]∧i2[5]=i2[6]∧a7588data[5]=a7588data[6]∧&&(&&(&&(&&(>=(i1942[5], 0), <(i1942[5], 42)), >(i1840[5], 0)), <(i1840[5], i2[5])), >(+(i1840[5], 1), 0))=TRUE ⇒ LOAD12814ARR2(java.lang.Object(ARRAY(i2[5], a7588data[5])), i1840[5], java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[5], o8443Field1[5], o8443Field2[5])), o8366[5], o8367[5])), NULL, o8367[5])), java.lang.Object(java.lang.String(i1942[5], i1941[5], i1943[5], a7876[5])))≥NonInfC∧LOAD12814ARR2(java.lang.Object(ARRAY(i2[5], a7588data[5])), i1840[5], java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[5], o8443Field1[5], o8443Field2[5])), o8366[5], o8367[5])), NULL, o8367[5])), java.lang.Object(java.lang.String(i1942[5], i1941[5], i1943[5], a7876[5])))≥COND_LOAD12814ARR2(&&(&&(&&(&&(>=(i1942[5], 0), <(i1942[5], 42)), >(i1840[5], 0)), <(i1840[5], i2[5])), >(+(i1840[5], 1), 0)), java.lang.Object(ARRAY(i2[5], a7588data[5])), i1840[5], java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[5], o8443Field1[5], o8443Field2[5])), o8366[5], o8367[5])), NULL, o8367[5])), java.lang.Object(java.lang.String(i1942[5], i1941[5], i1943[5], a7876[5])))∧(U^Increasing(COND_LOAD12814ARR2(&&(&&(&&(&&(>=(i1942[5], 0), <(i1942[5], 42)), >(i1840[5], 0)), <(i1840[5], i2[5])), >(+(i1840[5], 1), 0)), java.lang.Object(ARRAY(i2[5], a7588data[5])), i1840[5], java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[5], o8443Field1[5], o8443Field2[5])), o8366[5], o8367[5])), NULL, o8367[5])), java.lang.Object(java.lang.String(i1942[5], i1941[5], i1943[5], a7876[5])))), ≥))

We simplified constraint (30) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:
(31)    (>(+(i1840[5], 1), 0)=TRUE∧<(i1840[5], i2[5])=TRUE∧>(i1840[5], 0)=TRUE∧>=(i1942[5], 0)=TRUE∧<(i1942[5], 42)=TRUE ⇒ LOAD12814ARR2(java.lang.Object(ARRAY(i2[5], a7588data[5])), i1840[5], java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[5], o8443Field1[5], o8443Field2[5])), o8366[5], o8367[5])), NULL, o8367[5])), java.lang.Object(java.lang.String(i1942[5], i1941[5], i1943[5], a7876[5])))≥NonInfC∧LOAD12814ARR2(java.lang.Object(ARRAY(i2[5], a7588data[5])), i1840[5], java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[5], o8443Field1[5], o8443Field2[5])), o8366[5], o8367[5])), NULL, o8367[5])), java.lang.Object(java.lang.String(i1942[5], i1941[5], i1943[5], a7876[5])))≥COND_LOAD12814ARR2(&&(&&(&&(&&(>=(i1942[5], 0), <(i1942[5], 42)), >(i1840[5], 0)), <(i1840[5], i2[5])), >(+(i1840[5], 1), 0)), java.lang.Object(ARRAY(i2[5], a7588data[5])), i1840[5], java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[5], o8443Field1[5], o8443Field2[5])), o8366[5], o8367[5])), NULL, o8367[5])), java.lang.Object(java.lang.String(i1942[5], i1941[5], i1943[5], a7876[5])))∧(U^Increasing(COND_LOAD12814ARR2(&&(&&(&&(&&(>=(i1942[5], 0), <(i1942[5], 42)), >(i1840[5], 0)), <(i1840[5], i2[5])), >(+(i1840[5], 1), 0)), java.lang.Object(ARRAY(i2[5], a7588data[5])), i1840[5], java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[5], o8443Field1[5], o8443Field2[5])), o8366[5], o8367[5])), NULL, o8367[5])), java.lang.Object(java.lang.String(i1942[5], i1941[5], i1943[5], a7876[5])))), ≥))

We simplified constraint (31) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(32)    (i1840[5] ≥ 0∧i2[5] + [-1] + [-1]i1840[5] ≥ 0∧i1840[5] + [-1] ≥ 0∧i1942[5] ≥ 0∧[41] + [-1]i1942[5] ≥ 0 ⇒ (U^Increasing(COND_LOAD12814ARR2(&&(&&(&&(&&(>=(i1942[5], 0), <(i1942[5], 42)), >(i1840[5], 0)), <(i1840[5], i2[5])), >(+(i1840[5], 1), 0)), java.lang.Object(ARRAY(i2[5], a7588data[5])), i1840[5], java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[5], o8443Field1[5], o8443Field2[5])), o8366[5], o8367[5])), NULL, o8367[5])), java.lang.Object(java.lang.String(i1942[5], i1941[5], i1943[5], a7876[5])))), ≥)∧[(2)bni_40 + (-1)Bound*bni_40] + [(-1)bni_40]i1840[5] + [bni_40]i2[5] ≥ 0∧[1 + (-1)bso_41] ≥ 0)

We simplified constraint (32) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(33)    (i1840[5] ≥ 0∧i2[5] + [-1] + [-1]i1840[5] ≥ 0∧i1840[5] + [-1] ≥ 0∧i1942[5] ≥ 0∧[41] + [-1]i1942[5] ≥ 0 ⇒ (U^Increasing(COND_LOAD12814ARR2(&&(&&(&&(&&(>=(i1942[5], 0), <(i1942[5], 42)), >(i1840[5], 0)), <(i1840[5], i2[5])), >(+(i1840[5], 1), 0)), java.lang.Object(ARRAY(i2[5], a7588data[5])), i1840[5], java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[5], o8443Field1[5], o8443Field2[5])), o8366[5], o8367[5])), NULL, o8367[5])), java.lang.Object(java.lang.String(i1942[5], i1941[5], i1943[5], a7876[5])))), ≥)∧[(2)bni_40 + (-1)Bound*bni_40] + [(-1)bni_40]i1840[5] + [bni_40]i2[5] ≥ 0∧[1 + (-1)bso_41] ≥ 0)

We simplified constraint (33) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(34)    (i1840[5] ≥ 0∧i2[5] + [-1] + [-1]i1840[5] ≥ 0∧i1840[5] + [-1] ≥ 0∧i1942[5] ≥ 0∧[41] + [-1]i1942[5] ≥ 0 ⇒ (U^Increasing(COND_LOAD12814ARR2(&&(&&(&&(&&(>=(i1942[5], 0), <(i1942[5], 42)), >(i1840[5], 0)), <(i1840[5], i2[5])), >(+(i1840[5], 1), 0)), java.lang.Object(ARRAY(i2[5], a7588data[5])), i1840[5], java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[5], o8443Field1[5], o8443Field2[5])), o8366[5], o8367[5])), NULL, o8367[5])), java.lang.Object(java.lang.String(i1942[5], i1941[5], i1943[5], a7876[5])))), ≥)∧[(2)bni_40 + (-1)Bound*bni_40] + [(-1)bni_40]i1840[5] + [bni_40]i2[5] ≥ 0∧[1 + (-1)bso_41] ≥ 0)

We simplified constraint (34) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(35)    (i1840[5] ≥ 0∧i2[5] + [-1] + [-1]i1840[5] ≥ 0∧i1840[5] + [-1] ≥ 0∧i1942[5] ≥ 0∧[41] + [-1]i1942[5] ≥ 0 ⇒ (U^Increasing(COND_LOAD12814ARR2(&&(&&(&&(&&(>=(i1942[5], 0), <(i1942[5], 42)), >(i1840[5], 0)), <(i1840[5], i2[5])), >(+(i1840[5], 1), 0)), java.lang.Object(ARRAY(i2[5], a7588data[5])), i1840[5], java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[5], o8443Field1[5], o8443Field2[5])), o8366[5], o8367[5])), NULL, o8367[5])), java.lang.Object(java.lang.String(i1942[5], i1941[5], i1943[5], a7876[5])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(2)bni_40 + (-1)Bound*bni_40] + [(-1)bni_40]i1840[5] + [bni_40]i2[5] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_41] ≥ 0)

We simplified constraint (35) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(36)    ([1] + i1840[5] ≥ 0∧i2[5] + [-2] + [-1]i1840[5] ≥ 0∧i1840[5] ≥ 0∧i1942[5] ≥ 0∧[41] + [-1]i1942[5] ≥ 0 ⇒ (U^Increasing(COND_LOAD12814ARR2(&&(&&(&&(&&(>=(i1942[5], 0), <(i1942[5], 42)), >(i1840[5], 0)), <(i1840[5], i2[5])), >(+(i1840[5], 1), 0)), java.lang.Object(ARRAY(i2[5], a7588data[5])), i1840[5], java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[5], o8443Field1[5], o8443Field2[5])), o8366[5], o8367[5])), NULL, o8367[5])), java.lang.Object(java.lang.String(i1942[5], i1941[5], i1943[5], a7876[5])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[bni_40 + (-1)Bound*bni_40] + [(-1)bni_40]i1840[5] + [bni_40]i2[5] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_41] ≥ 0)

We simplified constraint (36) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(37)    ([1] + i1840[5] ≥ 0∧i2[5] ≥ 0∧i1840[5] ≥ 0∧i1942[5] ≥ 0∧[41] + [-1]i1942[5] ≥ 0 ⇒ (U^Increasing(COND_LOAD12814ARR2(&&(&&(&&(&&(>=(i1942[5], 0), <(i1942[5], 42)), >(i1840[5], 0)), <(i1840[5], i2[5])), >(+(i1840[5], 1), 0)), java.lang.Object(ARRAY(i2[5], a7588data[5])), i1840[5], java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[5], o8443Field1[5], o8443Field2[5])), o8366[5], o8367[5])), NULL, o8367[5])), java.lang.Object(java.lang.String(i1942[5], i1941[5], i1943[5], a7876[5])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(3)bni_40 + (-1)Bound*bni_40] + [bni_40]i2[5] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_41] ≥ 0)

For Pair COND_LOAD12814ARR2(TRUE, java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0, o8443Field1, o8443Field2)), o8366, o8367)), NULL, o8367)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876))) → LOAD12814(java.lang.Object(ARRAY(i2, a7588data)), +(i1840, 1), java.lang.Object(Tree(o8443Field0, o8443Field1, o8443Field2))) the following chains were created:

We consider the chain COND_LOAD12814ARR2(TRUE, java.lang.Object(ARRAY(i2[6], a7588data[6])), i1840[6], java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[6], o8443Field1[6], o8443Field2[6])), o8366[6], o8367[6])), NULL, o8367[6])), java.lang.Object(java.lang.String(i1942[6], i1941[6], i1943[6], a7876[6]))) → LOAD12814(java.lang.Object(ARRAY(i2[6], a7588data[6])), +(i1840[6], 1), java.lang.Object(Tree(o8443Field0[6], o8443Field1[6], o8443Field2[6]))) which results in the following constraint:
(38)    (COND_LOAD12814ARR2(TRUE, java.lang.Object(ARRAY(i2[6], a7588data[6])), i1840[6], java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[6], o8443Field1[6], o8443Field2[6])), o8366[6], o8367[6])), NULL, o8367[6])), java.lang.Object(java.lang.String(i1942[6], i1941[6], i1943[6], a7876[6])))≥NonInfC∧COND_LOAD12814ARR2(TRUE, java.lang.Object(ARRAY(i2[6], a7588data[6])), i1840[6], java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[6], o8443Field1[6], o8443Field2[6])), o8366[6], o8367[6])), NULL, o8367[6])), java.lang.Object(java.lang.String(i1942[6], i1941[6], i1943[6], a7876[6])))≥LOAD12814(java.lang.Object(ARRAY(i2[6], a7588data[6])), +(i1840[6], 1), java.lang.Object(Tree(o8443Field0[6], o8443Field1[6], o8443Field2[6])))∧(U^Increasing(LOAD12814(java.lang.Object(ARRAY(i2[6], a7588data[6])), +(i1840[6], 1), java.lang.Object(Tree(o8443Field0[6], o8443Field1[6], o8443Field2[6])))), ≥))

We simplified constraint (38) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(39)    ((U^Increasing(LOAD12814(java.lang.Object(ARRAY(i2[6], a7588data[6])), +(i1840[6], 1), java.lang.Object(Tree(o8443Field0[6], o8443Field1[6], o8443Field2[6])))), ≥)∧[(-1)bso_43] ≥ 0)

We simplified constraint (39) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(40)    ((U^Increasing(LOAD12814(java.lang.Object(ARRAY(i2[6], a7588data[6])), +(i1840[6], 1), java.lang.Object(Tree(o8443Field0[6], o8443Field1[6], o8443Field2[6])))), ≥)∧[(-1)bso_43] ≥ 0)

We simplified constraint (40) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(41)    ((U^Increasing(LOAD12814(java.lang.Object(ARRAY(i2[6], a7588data[6])), +(i1840[6], 1), java.lang.Object(Tree(o8443Field0[6], o8443Field1[6], o8443Field2[6])))), ≥)∧[(-1)bso_43] ≥ 0)

We simplified constraint (41) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(42)    ((U^Increasing(LOAD12814(java.lang.Object(ARRAY(i2[6], a7588data[6])), +(i1840[6], 1), java.lang.Object(Tree(o8443Field0[6], o8443Field1[6], o8443Field2[6])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_43] ≥ 0)

For Pair LOAD12814(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(NULL, o8366, o8367))) → LOAD12814ARR3(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(NULL, o8366, o8367)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876))) the following chains were created:

We consider the chain LOAD12814(java.lang.Object(ARRAY(i2[7], a7588data[7])), i1840[7], java.lang.Object(Tree(NULL, o8366[7], o8367[7]))) → LOAD12814ARR3(java.lang.Object(ARRAY(i2[7], a7588data[7])), i1840[7], java.lang.Object(Tree(NULL, o8366[7], o8367[7])), java.lang.Object(java.lang.String(i1942[7], i1941[7], i1943[7], a7876[7]))) which results in the following constraint:
(43)    (LOAD12814(java.lang.Object(ARRAY(i2[7], a7588data[7])), i1840[7], java.lang.Object(Tree(NULL, o8366[7], o8367[7])))≥NonInfC∧LOAD12814(java.lang.Object(ARRAY(i2[7], a7588data[7])), i1840[7], java.lang.Object(Tree(NULL, o8366[7], o8367[7])))≥LOAD12814ARR3(java.lang.Object(ARRAY(i2[7], a7588data[7])), i1840[7], java.lang.Object(Tree(NULL, o8366[7], o8367[7])), java.lang.Object(java.lang.String(i1942[7], i1941[7], i1943[7], a7876[7])))∧(U^Increasing(LOAD12814ARR3(java.lang.Object(ARRAY(i2[7], a7588data[7])), i1840[7], java.lang.Object(Tree(NULL, o8366[7], o8367[7])), java.lang.Object(java.lang.String(i1942[7], i1941[7], i1943[7], a7876[7])))), ≥))

We simplified constraint (43) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(44)    ((U^Increasing(LOAD12814ARR3(java.lang.Object(ARRAY(i2[7], a7588data[7])), i1840[7], java.lang.Object(Tree(NULL, o8366[7], o8367[7])), java.lang.Object(java.lang.String(i1942[7], i1941[7], i1943[7], a7876[7])))), ≥)∧[1 + (-1)bso_45] ≥ 0)

We simplified constraint (44) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(45)    ((U^Increasing(LOAD12814ARR3(java.lang.Object(ARRAY(i2[7], a7588data[7])), i1840[7], java.lang.Object(Tree(NULL, o8366[7], o8367[7])), java.lang.Object(java.lang.String(i1942[7], i1941[7], i1943[7], a7876[7])))), ≥)∧[1 + (-1)bso_45] ≥ 0)

We simplified constraint (45) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(46)    ((U^Increasing(LOAD12814ARR3(java.lang.Object(ARRAY(i2[7], a7588data[7])), i1840[7], java.lang.Object(Tree(NULL, o8366[7], o8367[7])), java.lang.Object(java.lang.String(i1942[7], i1941[7], i1943[7], a7876[7])))), ≥)∧[1 + (-1)bso_45] ≥ 0)

We simplified constraint (46) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(47)    ((U^Increasing(LOAD12814ARR3(java.lang.Object(ARRAY(i2[7], a7588data[7])), i1840[7], java.lang.Object(Tree(NULL, o8366[7], o8367[7])), java.lang.Object(java.lang.String(i1942[7], i1941[7], i1943[7], a7876[7])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_45] ≥ 0)

For Pair LOAD12814ARR3(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(NULL, o8366, o8367)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876))) → COND_LOAD12814ARR3(&&(&&(&&(&&(>=(i1942, 0), <(i1942, 42)), >(i1840, 0)), <(i1840, i2)), >(+(i1840, 1), 0)), java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(NULL, o8366, o8367)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876))) the following chains were created:

We consider the chain LOAD12814ARR3(java.lang.Object(ARRAY(i2[8], a7588data[8])), i1840[8], java.lang.Object(Tree(NULL, o8366[8], o8367[8])), java.lang.Object(java.lang.String(i1942[8], i1941[8], i1943[8], a7876[8]))) → COND_LOAD12814ARR3(&&(&&(&&(&&(>=(i1942[8], 0), <(i1942[8], 42)), >(i1840[8], 0)), <(i1840[8], i2[8])), >(+(i1840[8], 1), 0)), java.lang.Object(ARRAY(i2[8], a7588data[8])), i1840[8], java.lang.Object(Tree(NULL, o8366[8], o8367[8])), java.lang.Object(java.lang.String(i1942[8], i1941[8], i1943[8], a7876[8]))), COND_LOAD12814ARR3(TRUE, java.lang.Object(ARRAY(i2[9], a7588data[9])), i1840[9], java.lang.Object(Tree(NULL, o8366[9], o8367[9])), java.lang.Object(java.lang.String(i1942[9], i1941[9], i1943[9], a7876[9]))) → LOAD13105(java.lang.Object(ARRAY(i2[9], a7588data[9])), +(i1840[9], 1), java.lang.Object(Tree(NULL, o8366[9], o8367[9]))) which results in the following constraint:
(48)    (&&(&&(&&(&&(>=(i1942[8], 0), <(i1942[8], 42)), >(i1840[8], 0)), <(i1840[8], i2[8])), >(+(i1840[8], 1), 0))=TRUE∧i1840[8]=i1840[9]∧i2[8]=i2[9]∧a7588data[8]=a7588data[9]∧o8366[8]=o8366[9]∧o8367[8]=o8367[9]∧i1942[8]=i1942[9]∧i1941[8]=i1941[9]∧i1943[8]=i1943[9]∧a7876[8]=a7876[9] ⇒ LOAD12814ARR3(java.lang.Object(ARRAY(i2[8], a7588data[8])), i1840[8], java.lang.Object(Tree(NULL, o8366[8], o8367[8])), java.lang.Object(java.lang.String(i1942[8], i1941[8], i1943[8], a7876[8])))≥NonInfC∧LOAD12814ARR3(java.lang.Object(ARRAY(i2[8], a7588data[8])), i1840[8], java.lang.Object(Tree(NULL, o8366[8], o8367[8])), java.lang.Object(java.lang.String(i1942[8], i1941[8], i1943[8], a7876[8])))≥COND_LOAD12814ARR3(&&(&&(&&(&&(>=(i1942[8], 0), <(i1942[8], 42)), >(i1840[8], 0)), <(i1840[8], i2[8])), >(+(i1840[8], 1), 0)), java.lang.Object(ARRAY(i2[8], a7588data[8])), i1840[8], java.lang.Object(Tree(NULL, o8366[8], o8367[8])), java.lang.Object(java.lang.String(i1942[8], i1941[8], i1943[8], a7876[8])))∧(U^Increasing(COND_LOAD12814ARR3(&&(&&(&&(&&(>=(i1942[8], 0), <(i1942[8], 42)), >(i1840[8], 0)), <(i1840[8], i2[8])), >(+(i1840[8], 1), 0)), java.lang.Object(ARRAY(i2[8], a7588data[8])), i1840[8], java.lang.Object(Tree(NULL, o8366[8], o8367[8])), java.lang.Object(java.lang.String(i1942[8], i1941[8], i1943[8], a7876[8])))), ≥))

We simplified constraint (48) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:
(49)    (>(+(i1840[8], 1), 0)=TRUE∧<(i1840[8], i2[8])=TRUE∧>(i1840[8], 0)=TRUE∧>=(i1942[8], 0)=TRUE∧<(i1942[8], 42)=TRUE ⇒ LOAD12814ARR3(java.lang.Object(ARRAY(i2[8], a7588data[8])), i1840[8], java.lang.Object(Tree(NULL, o8366[8], o8367[8])), java.lang.Object(java.lang.String(i1942[8], i1941[8], i1943[8], a7876[8])))≥NonInfC∧LOAD12814ARR3(java.lang.Object(ARRAY(i2[8], a7588data[8])), i1840[8], java.lang.Object(Tree(NULL, o8366[8], o8367[8])), java.lang.Object(java.lang.String(i1942[8], i1941[8], i1943[8], a7876[8])))≥COND_LOAD12814ARR3(&&(&&(&&(&&(>=(i1942[8], 0), <(i1942[8], 42)), >(i1840[8], 0)), <(i1840[8], i2[8])), >(+(i1840[8], 1), 0)), java.lang.Object(ARRAY(i2[8], a7588data[8])), i1840[8], java.lang.Object(Tree(NULL, o8366[8], o8367[8])), java.lang.Object(java.lang.String(i1942[8], i1941[8], i1943[8], a7876[8])))∧(U^Increasing(COND_LOAD12814ARR3(&&(&&(&&(&&(>=(i1942[8], 0), <(i1942[8], 42)), >(i1840[8], 0)), <(i1840[8], i2[8])), >(+(i1840[8], 1), 0)), java.lang.Object(ARRAY(i2[8], a7588data[8])), i1840[8], java.lang.Object(Tree(NULL, o8366[8], o8367[8])), java.lang.Object(java.lang.String(i1942[8], i1941[8], i1943[8], a7876[8])))), ≥))

We simplified constraint (49) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(50)    (i1840[8] ≥ 0∧i2[8] + [-1] + [-1]i1840[8] ≥ 0∧i1840[8] + [-1] ≥ 0∧i1942[8] ≥ 0∧[41] + [-1]i1942[8] ≥ 0 ⇒ (U^Increasing(COND_LOAD12814ARR3(&&(&&(&&(&&(>=(i1942[8], 0), <(i1942[8], 42)), >(i1840[8], 0)), <(i1840[8], i2[8])), >(+(i1840[8], 1), 0)), java.lang.Object(ARRAY(i2[8], a7588data[8])), i1840[8], java.lang.Object(Tree(NULL, o8366[8], o8367[8])), java.lang.Object(java.lang.String(i1942[8], i1941[8], i1943[8], a7876[8])))), ≥)∧[bni_46 + (-1)Bound*bni_46] + [(-1)bni_46]i1840[8] + [bni_46]i2[8] ≥ 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (50) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(51)    (i1840[8] ≥ 0∧i2[8] + [-1] + [-1]i1840[8] ≥ 0∧i1840[8] + [-1] ≥ 0∧i1942[8] ≥ 0∧[41] + [-1]i1942[8] ≥ 0 ⇒ (U^Increasing(COND_LOAD12814ARR3(&&(&&(&&(&&(>=(i1942[8], 0), <(i1942[8], 42)), >(i1840[8], 0)), <(i1840[8], i2[8])), >(+(i1840[8], 1), 0)), java.lang.Object(ARRAY(i2[8], a7588data[8])), i1840[8], java.lang.Object(Tree(NULL, o8366[8], o8367[8])), java.lang.Object(java.lang.String(i1942[8], i1941[8], i1943[8], a7876[8])))), ≥)∧[bni_46 + (-1)Bound*bni_46] + [(-1)bni_46]i1840[8] + [bni_46]i2[8] ≥ 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (51) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(52)    (i1840[8] ≥ 0∧i2[8] + [-1] + [-1]i1840[8] ≥ 0∧i1840[8] + [-1] ≥ 0∧i1942[8] ≥ 0∧[41] + [-1]i1942[8] ≥ 0 ⇒ (U^Increasing(COND_LOAD12814ARR3(&&(&&(&&(&&(>=(i1942[8], 0), <(i1942[8], 42)), >(i1840[8], 0)), <(i1840[8], i2[8])), >(+(i1840[8], 1), 0)), java.lang.Object(ARRAY(i2[8], a7588data[8])), i1840[8], java.lang.Object(Tree(NULL, o8366[8], o8367[8])), java.lang.Object(java.lang.String(i1942[8], i1941[8], i1943[8], a7876[8])))), ≥)∧[bni_46 + (-1)Bound*bni_46] + [(-1)bni_46]i1840[8] + [bni_46]i2[8] ≥ 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (52) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(53)    (i1840[8] ≥ 0∧i2[8] + [-1] + [-1]i1840[8] ≥ 0∧i1840[8] + [-1] ≥ 0∧i1942[8] ≥ 0∧[41] + [-1]i1942[8] ≥ 0 ⇒ (U^Increasing(COND_LOAD12814ARR3(&&(&&(&&(&&(>=(i1942[8], 0), <(i1942[8], 42)), >(i1840[8], 0)), <(i1840[8], i2[8])), >(+(i1840[8], 1), 0)), java.lang.Object(ARRAY(i2[8], a7588data[8])), i1840[8], java.lang.Object(Tree(NULL, o8366[8], o8367[8])), java.lang.Object(java.lang.String(i1942[8], i1941[8], i1943[8], a7876[8])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[bni_46 + (-1)Bound*bni_46] + [(-1)bni_46]i1840[8] + [bni_46]i2[8] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (53) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(54)    ([1] + i1840[8] ≥ 0∧i2[8] + [-2] + [-1]i1840[8] ≥ 0∧i1840[8] ≥ 0∧i1942[8] ≥ 0∧[41] + [-1]i1942[8] ≥ 0 ⇒ (U^Increasing(COND_LOAD12814ARR3(&&(&&(&&(&&(>=(i1942[8], 0), <(i1942[8], 42)), >(i1840[8], 0)), <(i1840[8], i2[8])), >(+(i1840[8], 1), 0)), java.lang.Object(ARRAY(i2[8], a7588data[8])), i1840[8], java.lang.Object(Tree(NULL, o8366[8], o8367[8])), java.lang.Object(java.lang.String(i1942[8], i1941[8], i1943[8], a7876[8])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)Bound*bni_46] + [(-1)bni_46]i1840[8] + [bni_46]i2[8] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (54) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(55)    ([1] + i1840[8] ≥ 0∧i2[8] ≥ 0∧i1840[8] ≥ 0∧i1942[8] ≥ 0∧[41] + [-1]i1942[8] ≥ 0 ⇒ (U^Increasing(COND_LOAD12814ARR3(&&(&&(&&(&&(>=(i1942[8], 0), <(i1942[8], 42)), >(i1840[8], 0)), <(i1840[8], i2[8])), >(+(i1840[8], 1), 0)), java.lang.Object(ARRAY(i2[8], a7588data[8])), i1840[8], java.lang.Object(Tree(NULL, o8366[8], o8367[8])), java.lang.Object(java.lang.String(i1942[8], i1941[8], i1943[8], a7876[8])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)Bound*bni_46 + (2)bni_46] + [bni_46]i2[8] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_47] ≥ 0)

For Pair COND_LOAD12814ARR3(TRUE, java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(NULL, o8366, o8367)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876))) → LOAD13105(java.lang.Object(ARRAY(i2, a7588data)), +(i1840, 1), java.lang.Object(Tree(NULL, o8366, o8367))) the following chains were created:

We consider the chain COND_LOAD12814ARR3(TRUE, java.lang.Object(ARRAY(i2[9], a7588data[9])), i1840[9], java.lang.Object(Tree(NULL, o8366[9], o8367[9])), java.lang.Object(java.lang.String(i1942[9], i1941[9], i1943[9], a7876[9]))) → LOAD13105(java.lang.Object(ARRAY(i2[9], a7588data[9])), +(i1840[9], 1), java.lang.Object(Tree(NULL, o8366[9], o8367[9]))) which results in the following constraint:
(56)    (COND_LOAD12814ARR3(TRUE, java.lang.Object(ARRAY(i2[9], a7588data[9])), i1840[9], java.lang.Object(Tree(NULL, o8366[9], o8367[9])), java.lang.Object(java.lang.String(i1942[9], i1941[9], i1943[9], a7876[9])))≥NonInfC∧COND_LOAD12814ARR3(TRUE, java.lang.Object(ARRAY(i2[9], a7588data[9])), i1840[9], java.lang.Object(Tree(NULL, o8366[9], o8367[9])), java.lang.Object(java.lang.String(i1942[9], i1941[9], i1943[9], a7876[9])))≥LOAD13105(java.lang.Object(ARRAY(i2[9], a7588data[9])), +(i1840[9], 1), java.lang.Object(Tree(NULL, o8366[9], o8367[9])))∧(U^Increasing(LOAD13105(java.lang.Object(ARRAY(i2[9], a7588data[9])), +(i1840[9], 1), java.lang.Object(Tree(NULL, o8366[9], o8367[9])))), ≥))

We simplified constraint (56) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(57)    ((U^Increasing(LOAD13105(java.lang.Object(ARRAY(i2[9], a7588data[9])), +(i1840[9], 1), java.lang.Object(Tree(NULL, o8366[9], o8367[9])))), ≥)∧[(-1)bso_49] ≥ 0)

We simplified constraint (57) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(58)    ((U^Increasing(LOAD13105(java.lang.Object(ARRAY(i2[9], a7588data[9])), +(i1840[9], 1), java.lang.Object(Tree(NULL, o8366[9], o8367[9])))), ≥)∧[(-1)bso_49] ≥ 0)

We simplified constraint (58) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(59)    ((U^Increasing(LOAD13105(java.lang.Object(ARRAY(i2[9], a7588data[9])), +(i1840[9], 1), java.lang.Object(Tree(NULL, o8366[9], o8367[9])))), ≥)∧[(-1)bso_49] ≥ 0)

We simplified constraint (59) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(60)    ((U^Increasing(LOAD13105(java.lang.Object(ARRAY(i2[9], a7588data[9])), +(i1840[9], 1), java.lang.Object(Tree(NULL, o8366[9], o8367[9])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_49] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

LOAD13105(java.lang.Object(ARRAY(i2, a7588data)), i1876, java.lang.Object(Tree(o8359, java.lang.Object(Tree(o8442Field0, o8442Field1, o8442Field2)), o8361))) → LOAD12814(java.lang.Object(ARRAY(i2, a7588data)), i1876, java.lang.Object(Tree(o8442Field0, o8442Field1, o8442Field2)))
- ((U^Increasing(LOAD12814(java.lang.Object(ARRAY(i2[0], a7588data[0])), i1876[0], java.lang.Object(Tree(o8442Field0[0], o8442Field1[0], o8442Field2[0])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_31] ≥ 0)
LOAD12814(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(o8359, java.lang.Object(Tree(o8442Field0, o8442Field1, o8442Field2)), o8361))) → LOAD12814ARR1(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(o8359, java.lang.Object(Tree(o8442Field0, o8442Field1, o8442Field2)), o8361)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876)))
- ((U^Increasing(LOAD12814ARR1(java.lang.Object(ARRAY(i2[1], a7588data[1])), i1840[1], java.lang.Object(Tree(o8359[1], java.lang.Object(Tree(o8442Field0[1], o8442Field1[1], o8442Field2[1])), o8361[1])), java.lang.Object(java.lang.String(i1942[1], i1941[1], i1943[1], a7876[1])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_33] ≥ 0)
LOAD12814ARR1(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359, java.lang.Object(Tree(o8442Field0, o8442Field1, o8442Field2)), o8361)), o8361)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876))) → COND_LOAD12814ARR1(&&(&&(&&(>=(i1942, 42), >(i1840, 0)), <(i1840, i2)), >(+(i1840, 1), 0)), java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359, java.lang.Object(Tree(o8442Field0, o8442Field1, o8442Field2)), o8361)), o8361)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876)))
- ([1] + i1840[2] ≥ 0∧i2[2] ≥ 0∧i1942[2] ≥ 0∧i1840[2] ≥ 0 ⇒ (U^Increasing(COND_LOAD12814ARR1(&&(&&(&&(>=(i1942[2], 42), >(i1840[2], 0)), <(i1840[2], i2[2])), >(+(i1840[2], 1), 0)), java.lang.Object(ARRAY(i2[2], a7588data[2])), i1840[2], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[2], java.lang.Object(Tree(o8442Field0[2], o8442Field1[2], o8442Field2[2])), o8361[2])), o8361[2])), java.lang.Object(java.lang.String(i1942[2], i1941[2], i1943[2], a7876[2])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)Bound*bni_34 + (2)bni_34] + [bni_34]i2[2] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)
COND_LOAD12814ARR1(TRUE, java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359, java.lang.Object(Tree(o8442Field0, o8442Field1, o8442Field2)), o8361)), o8361)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876))) → LOAD12814(java.lang.Object(ARRAY(i2, a7588data)), +(i1840, 1), java.lang.Object(Tree(o8442Field0, o8442Field1, o8442Field2)))
- ((U^Increasing(LOAD12814(java.lang.Object(ARRAY(i2[3], a7588data[3])), +(i1840[3], 1), java.lang.Object(Tree(o8442Field0[3], o8442Field1[3], o8442Field2[3])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_37] ≥ 0)
LOAD12814(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0, o8443Field1, o8443Field2)), o8366, o8367))) → LOAD12814ARR2(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0, o8443Field1, o8443Field2)), o8366, o8367)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876)))
- ((U^Increasing(LOAD12814ARR2(java.lang.Object(ARRAY(i2[4], a7588data[4])), i1840[4], java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[4], o8443Field1[4], o8443Field2[4])), o8366[4], o8367[4])), java.lang.Object(java.lang.String(i1942[4], i1941[4], i1943[4], a7876[4])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_39] ≥ 0)
LOAD12814ARR2(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0, o8443Field1, o8443Field2)), o8366, o8367)), NULL, o8367)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876))) → COND_LOAD12814ARR2(&&(&&(&&(&&(>=(i1942, 0), <(i1942, 42)), >(i1840, 0)), <(i1840, i2)), >(+(i1840, 1), 0)), java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0, o8443Field1, o8443Field2)), o8366, o8367)), NULL, o8367)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876)))
- ([1] + i1840[5] ≥ 0∧i2[5] ≥ 0∧i1840[5] ≥ 0∧i1942[5] ≥ 0∧[41] + [-1]i1942[5] ≥ 0 ⇒ (U^Increasing(COND_LOAD12814ARR2(&&(&&(&&(&&(>=(i1942[5], 0), <(i1942[5], 42)), >(i1840[5], 0)), <(i1840[5], i2[5])), >(+(i1840[5], 1), 0)), java.lang.Object(ARRAY(i2[5], a7588data[5])), i1840[5], java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[5], o8443Field1[5], o8443Field2[5])), o8366[5], o8367[5])), NULL, o8367[5])), java.lang.Object(java.lang.String(i1942[5], i1941[5], i1943[5], a7876[5])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(3)bni_40 + (-1)Bound*bni_40] + [bni_40]i2[5] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_41] ≥ 0)
COND_LOAD12814ARR2(TRUE, java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0, o8443Field1, o8443Field2)), o8366, o8367)), NULL, o8367)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876))) → LOAD12814(java.lang.Object(ARRAY(i2, a7588data)), +(i1840, 1), java.lang.Object(Tree(o8443Field0, o8443Field1, o8443Field2)))
- ((U^Increasing(LOAD12814(java.lang.Object(ARRAY(i2[6], a7588data[6])), +(i1840[6], 1), java.lang.Object(Tree(o8443Field0[6], o8443Field1[6], o8443Field2[6])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_43] ≥ 0)
LOAD12814(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(NULL, o8366, o8367))) → LOAD12814ARR3(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(NULL, o8366, o8367)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876)))
- ((U^Increasing(LOAD12814ARR3(java.lang.Object(ARRAY(i2[7], a7588data[7])), i1840[7], java.lang.Object(Tree(NULL, o8366[7], o8367[7])), java.lang.Object(java.lang.String(i1942[7], i1941[7], i1943[7], a7876[7])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_45] ≥ 0)
LOAD12814ARR3(java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(NULL, o8366, o8367)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876))) → COND_LOAD12814ARR3(&&(&&(&&(&&(>=(i1942, 0), <(i1942, 42)), >(i1840, 0)), <(i1840, i2)), >(+(i1840, 1), 0)), java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(NULL, o8366, o8367)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876)))
- ([1] + i1840[8] ≥ 0∧i2[8] ≥ 0∧i1840[8] ≥ 0∧i1942[8] ≥ 0∧[41] + [-1]i1942[8] ≥ 0 ⇒ (U^Increasing(COND_LOAD12814ARR3(&&(&&(&&(&&(>=(i1942[8], 0), <(i1942[8], 42)), >(i1840[8], 0)), <(i1840[8], i2[8])), >(+(i1840[8], 1), 0)), java.lang.Object(ARRAY(i2[8], a7588data[8])), i1840[8], java.lang.Object(Tree(NULL, o8366[8], o8367[8])), java.lang.Object(java.lang.String(i1942[8], i1941[8], i1943[8], a7876[8])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)Bound*bni_46 + (2)bni_46] + [bni_46]i2[8] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_47] ≥ 0)
COND_LOAD12814ARR3(TRUE, java.lang.Object(ARRAY(i2, a7588data)), i1840, java.lang.Object(Tree(NULL, o8366, o8367)), java.lang.Object(java.lang.String(i1942, i1941, i1943, a7876))) → LOAD13105(java.lang.Object(ARRAY(i2, a7588data)), +(i1840, 1), java.lang.Object(Tree(NULL, o8366, o8367)))
- ((U^Increasing(LOAD13105(java.lang.Object(ARRAY(i2[9], a7588data[9])), +(i1840[9], 1), java.lang.Object(Tree(NULL, o8366[9], o8367[9])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_49] ≥ 0)

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0
POL(FALSE) = 0
POL(LOAD13105(x₁, x₂, x₃)) = [1] + [-1]x₂ + [-1]x₁
POL(java.lang.Object(x₁)) = x₁
POL(ARRAY(x₁, x₂)) = [-1] + [-1]x₁
POL(Tree(x₁, x₂, x₃)) = [-1]
POL(LOAD12814(x₁, x₂, x₃)) = [1] + [-1]x₂ + [-1]x₁
POL(LOAD12814ARR1(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₄ + [-1]x₂ + [-1]x₁
POL(java.lang.String(x₁, x₂, x₃, x₄)) = [-1]
POL(NULL) = [-1]
POL(COND_LOAD12814ARR1(x₁, x₂, x₃, x₄, x₅)) = [-1] + [-1]x₅ + [-1]x₃ + [-1]x₂
POL(&&(x₁, x₂)) = [-1]
POL(>=(x₁, x₂)) = [-1]
POL(42) = [42]
POL(>(x₁, x₂)) = [-1]
POL(0) = 0
POL(<(x₁, x₂)) = [-1]
POL(+(x₁, x₂)) = x₁ + x₂
POL(1) = [1]
POL(LOAD12814ARR2(x₁, x₂, x₃, x₄)) = [1] + [-1]x₂ + [-1]x₁
POL(COND_LOAD12814ARR2(x₁, x₂, x₃, x₄, x₅)) = [-1]x₃ + [-1]x₂
POL(LOAD12814ARR3(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₄ + [-1]x₂ + [-1]x₁
POL(COND_LOAD12814ARR3(x₁, x₂, x₃, x₄, x₅)) = [-1] + [-1]x₅ + [-1]x₃ + [-1]x₂

The following pairs are in P_>:

LOAD12814(java.lang.Object(ARRAY(i2[1], a7588data[1])), i1840[1], java.lang.Object(Tree(o8359[1], java.lang.Object(Tree(o8442Field0[1], o8442Field1[1], o8442Field2[1])), o8361[1]))) → LOAD12814ARR1(java.lang.Object(ARRAY(i2[1], a7588data[1])), i1840[1], java.lang.Object(Tree(o8359[1], java.lang.Object(Tree(o8442Field0[1], o8442Field1[1], o8442Field2[1])), o8361[1])), java.lang.Object(java.lang.String(i1942[1], i1941[1], i1943[1], a7876[1])))
LOAD12814ARR2(java.lang.Object(ARRAY(i2[5], a7588data[5])), i1840[5], java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[5], o8443Field1[5], o8443Field2[5])), o8366[5], o8367[5])), NULL, o8367[5])), java.lang.Object(java.lang.String(i1942[5], i1941[5], i1943[5], a7876[5]))) → COND_LOAD12814ARR2(&&(&&(&&(&&(>=(i1942[5], 0), <(i1942[5], 42)), >(i1840[5], 0)), <(i1840[5], i2[5])), >(+(i1840[5], 1), 0)), java.lang.Object(ARRAY(i2[5], a7588data[5])), i1840[5], java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[5], o8443Field1[5], o8443Field2[5])), o8366[5], o8367[5])), NULL, o8367[5])), java.lang.Object(java.lang.String(i1942[5], i1941[5], i1943[5], a7876[5])))
LOAD12814(java.lang.Object(ARRAY(i2[7], a7588data[7])), i1840[7], java.lang.Object(Tree(NULL, o8366[7], o8367[7]))) → LOAD12814ARR3(java.lang.Object(ARRAY(i2[7], a7588data[7])), i1840[7], java.lang.Object(Tree(NULL, o8366[7], o8367[7])), java.lang.Object(java.lang.String(i1942[7], i1941[7], i1943[7], a7876[7])))

The following pairs are in P_bound:

LOAD12814ARR1(java.lang.Object(ARRAY(i2[2], a7588data[2])), i1840[2], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[2], java.lang.Object(Tree(o8442Field0[2], o8442Field1[2], o8442Field2[2])), o8361[2])), o8361[2])), java.lang.Object(java.lang.String(i1942[2], i1941[2], i1943[2], a7876[2]))) → COND_LOAD12814ARR1(&&(&&(&&(>=(i1942[2], 42), >(i1840[2], 0)), <(i1840[2], i2[2])), >(+(i1840[2], 1), 0)), java.lang.Object(ARRAY(i2[2], a7588data[2])), i1840[2], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[2], java.lang.Object(Tree(o8442Field0[2], o8442Field1[2], o8442Field2[2])), o8361[2])), o8361[2])), java.lang.Object(java.lang.String(i1942[2], i1941[2], i1943[2], a7876[2])))
LOAD12814ARR2(java.lang.Object(ARRAY(i2[5], a7588data[5])), i1840[5], java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[5], o8443Field1[5], o8443Field2[5])), o8366[5], o8367[5])), NULL, o8367[5])), java.lang.Object(java.lang.String(i1942[5], i1941[5], i1943[5], a7876[5]))) → COND_LOAD12814ARR2(&&(&&(&&(&&(>=(i1942[5], 0), <(i1942[5], 42)), >(i1840[5], 0)), <(i1840[5], i2[5])), >(+(i1840[5], 1), 0)), java.lang.Object(ARRAY(i2[5], a7588data[5])), i1840[5], java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[5], o8443Field1[5], o8443Field2[5])), o8366[5], o8367[5])), NULL, o8367[5])), java.lang.Object(java.lang.String(i1942[5], i1941[5], i1943[5], a7876[5])))
LOAD12814ARR3(java.lang.Object(ARRAY(i2[8], a7588data[8])), i1840[8], java.lang.Object(Tree(NULL, o8366[8], o8367[8])), java.lang.Object(java.lang.String(i1942[8], i1941[8], i1943[8], a7876[8]))) → COND_LOAD12814ARR3(&&(&&(&&(&&(>=(i1942[8], 0), <(i1942[8], 42)), >(i1840[8], 0)), <(i1840[8], i2[8])), >(+(i1840[8], 1), 0)), java.lang.Object(ARRAY(i2[8], a7588data[8])), i1840[8], java.lang.Object(Tree(NULL, o8366[8], o8367[8])), java.lang.Object(java.lang.String(i1942[8], i1941[8], i1943[8], a7876[8])))

The following pairs are in P_≥:

LOAD13105(java.lang.Object(ARRAY(i2[0], a7588data[0])), i1876[0], java.lang.Object(Tree(o8359[0], java.lang.Object(Tree(o8442Field0[0], o8442Field1[0], o8442Field2[0])), o8361[0]))) → LOAD12814(java.lang.Object(ARRAY(i2[0], a7588data[0])), i1876[0], java.lang.Object(Tree(o8442Field0[0], o8442Field1[0], o8442Field2[0])))
LOAD12814ARR1(java.lang.Object(ARRAY(i2[2], a7588data[2])), i1840[2], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[2], java.lang.Object(Tree(o8442Field0[2], o8442Field1[2], o8442Field2[2])), o8361[2])), o8361[2])), java.lang.Object(java.lang.String(i1942[2], i1941[2], i1943[2], a7876[2]))) → COND_LOAD12814ARR1(&&(&&(&&(>=(i1942[2], 42), >(i1840[2], 0)), <(i1840[2], i2[2])), >(+(i1840[2], 1), 0)), java.lang.Object(ARRAY(i2[2], a7588data[2])), i1840[2], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[2], java.lang.Object(Tree(o8442Field0[2], o8442Field1[2], o8442Field2[2])), o8361[2])), o8361[2])), java.lang.Object(java.lang.String(i1942[2], i1941[2], i1943[2], a7876[2])))
COND_LOAD12814ARR1(TRUE, java.lang.Object(ARRAY(i2[3], a7588data[3])), i1840[3], java.lang.Object(Tree(NULL, java.lang.Object(Tree(o8359[3], java.lang.Object(Tree(o8442Field0[3], o8442Field1[3], o8442Field2[3])), o8361[3])), o8361[3])), java.lang.Object(java.lang.String(i1942[3], i1941[3], i1943[3], a7876[3]))) → LOAD12814(java.lang.Object(ARRAY(i2[3], a7588data[3])), +(i1840[3], 1), java.lang.Object(Tree(o8442Field0[3], o8442Field1[3], o8442Field2[3])))
LOAD12814(java.lang.Object(ARRAY(i2[4], a7588data[4])), i1840[4], java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[4], o8443Field1[4], o8443Field2[4])), o8366[4], o8367[4]))) → LOAD12814ARR2(java.lang.Object(ARRAY(i2[4], a7588data[4])), i1840[4], java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[4], o8443Field1[4], o8443Field2[4])), o8366[4], o8367[4])), java.lang.Object(java.lang.String(i1942[4], i1941[4], i1943[4], a7876[4])))
COND_LOAD12814ARR2(TRUE, java.lang.Object(ARRAY(i2[6], a7588data[6])), i1840[6], java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(o8443Field0[6], o8443Field1[6], o8443Field2[6])), o8366[6], o8367[6])), NULL, o8367[6])), java.lang.Object(java.lang.String(i1942[6], i1941[6], i1943[6], a7876[6]))) → LOAD12814(java.lang.Object(ARRAY(i2[6], a7588data[6])), +(i1840[6], 1), java.lang.Object(Tree(o8443Field0[6], o8443Field1[6], o8443Field2[6])))
LOAD12814ARR3(java.lang.Object(ARRAY(i2[8], a7588data[8])), i1840[8], java.lang.Object(Tree(NULL, o8366[8], o8367[8])), java.lang.Object(java.lang.String(i1942[8], i1941[8], i1943[8], a7876[8]))) → COND_LOAD12814ARR3(&&(&&(&&(&&(>=(i1942[8], 0), <(i1942[8], 42)), >(i1840[8], 0)), <(i1840[8], i2[8])), >(+(i1840[8], 1), 0)), java.lang.Object(ARRAY(i2[8], a7588data[8])), i1840[8], java.lang.Object(Tree(NULL, o8366[8], o8367[8])), java.lang.Object(java.lang.String(i1942[8], i1941[8], i1943[8], a7876[8])))
COND_LOAD12814ARR3(TRUE, java.lang.Object(ARRAY(i2[9], a7588data[9])), i1840[9], java.lang.Object(Tree(NULL, o8366[9], o8367[9])), java.lang.Object(java.lang.String(i1942[9], i1941[9], i1943[9], a7876[9]))) → LOAD13105(java.lang.Object(ARRAY(i2[9], a7588data[9])), +(i1840[9], 1), java.lang.Object(Tree(NULL, o8366[9], o8367[9])))

There are no usable rules.

(13) Complex Obligation (AND)

(14) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

(15) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 7 less nodes.

(16) TRUE

(17) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

(18) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 7 less nodes.

(19) TRUE

(20) Obligation:

ITRS problem:

The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, java.lang.Object(Tree(o5839Field0, o5839Field1, o5839Field2)), java.lang.Object(EOC))), java.lang.Object(Tree(o5204, java.lang.Object(Tree(o5839Field0, o5839Field1, o5839Field2)), java.lang.Object(EOC)))) → Load7791ARR4(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, java.lang.Object(Tree(o5839Field0, o5839Field1, o5839Field2)), java.lang.Object(EOC))), java.lang.Object(Tree(o5204, java.lang.Object(Tree(o5839Field0, o5839Field1, o5839Field2)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i1289, i1291, a5451)))
Load7791ARR4(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, java.lang.Object(Tree(o5839Field0, o5839Field1, o5839Field2)), java.lang.Object(EOC))), java.lang.Object(Tree(o5204, java.lang.Object(Tree(o5839Field0, o5839Field1, o5839Field2)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i1289, i1291, a5451))) → Cond_Load7791ARR4(i1253 > 0 && i1253 < i2 && i1255 > 0 && i1253 + 1 > 0, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, java.lang.Object(Tree(o5839Field0, o5839Field1, o5839Field2)), java.lang.Object(EOC))), java.lang.Object(Tree(o5204, java.lang.Object(Tree(o5839Field0, o5839Field1, o5839Field2)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i1289, i1291, a5451)))
Cond_Load7791ARR4(TRUE, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, java.lang.Object(Tree(o5839Field0, o5839Field1, o5839Field2)), java.lang.Object(EOC))), java.lang.Object(Tree(o5204, java.lang.Object(Tree(o5839Field0, o5839Field1, o5839Field2)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i1289, i1291, a5451))) → Inc9967(java.lang.Object(ARRAY(i2, a5234data)), i1253 + 1, i1255, java.lang.Object(Tree(o5204, java.lang.Object(Tree(o5839Field0, o5839Field1, o5839Field2)), java.lang.Object(EOC))), java.lang.Object(Tree(o5839Field0, o5839Field1, o5839Field2)))
JMP10050(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5950Field0, o5950Field1, o5950Field2))) → Inc9967(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5950Field0, o5950Field1, o5950Field2)))
Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o5950Field0, o5950Field1, o5950Field2)), o5783, o5784))) → Load7791ARR5(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o5950Field0, o5950Field1, o5950Field2)), o5783, o5784)), java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451)))
Load7791ARR5(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o5950Field0, o5950Field1, o5950Field2)), o5783, o5784)), java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451))) → Cond_Load7791ARR5(i1334 > 0 && i1253 > 0 && i1253 < i2 && i1255 > 0 && i1253 + 1 > 0, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o5950Field0, o5950Field1, o5950Field2)), o5783, o5784)), java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451)))
Cond_Load7791ARR5(TRUE, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o5950Field0, o5950Field1, o5950Field2)), o5783, o5784)), java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451))) → Inc9967(java.lang.Object(ARRAY(i2, a5234data)), i1253 + 1, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5950Field0, o5950Field1, o5950Field2)))
Inc9967(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5931Field0, o5931Field1, o5931Field2))) → Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255 + -1, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5931Field0, o5931Field1, o5931Field2)))
Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5775, java.lang.Object(Tree(o5931Field0, o5931Field1, o5931Field2)), o5777))) → Load7791ARR6(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5775, java.lang.Object(Tree(o5931Field0, o5931Field1, o5931Field2)), o5777)), java.lang.Object(java.lang.String(0, i1289, i1291, a5451)))
Load7791ARR6(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5775, java.lang.Object(Tree(o5931Field0, o5931Field1, o5931Field2)), o5777)), java.lang.Object(java.lang.String(0, i1289, i1291, a5451))) → Cond_Load7791ARR6(i1253 > 0 && i1253 < i2 && i1255 > 0 && i1253 + 1 > 0, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5775, java.lang.Object(Tree(o5931Field0, o5931Field1, o5931Field2)), o5777)), java.lang.Object(java.lang.String(0, i1289, i1291, a5451)))
Cond_Load7791ARR6(TRUE, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5775, java.lang.Object(Tree(o5931Field0, o5931Field1, o5931Field2)), o5777)), java.lang.Object(java.lang.String(0, i1289, i1291, a5451))) → Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253 + 1, i1255 + -1, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5931Field0, o5931Field1, o5931Field2)))
Inc12523(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC)))) → Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255 + -1, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))))
JMP12428(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC)))) → Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255 + -1, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))))
Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5775, NULL, o5777))) → Load7791ARR7(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5775, NULL, o5777)), java.lang.Object(java.lang.String(0, i1289, i1291, a5451)))
Load7791ARR7(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5775, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o5777)), java.lang.Object(java.lang.String(0, i1289, i1291, a5451))) → Cond_Load7791ARR7(i1253 > 0 && i1253 < i2 && i1255 > 0 && i1253 + 1 > 0, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5775, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o5777)), java.lang.Object(java.lang.String(0, i1289, i1291, a5451)))
Cond_Load7791ARR7(TRUE, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5775, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o5777)), java.lang.Object(java.lang.String(0, i1289, i1291, a5451))) → Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253 + 1, i1255 + -1, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))))
Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(java.lang.Object(Tree(o5882Field0, o5882Field1, o5882Field2)), o5205, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o5882Field0, o5882Field1, o5882Field2)), o5205, java.lang.Object(EOC)))) → Load7791ARR8(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(java.lang.Object(Tree(o5882Field0, o5882Field1, o5882Field2)), o5205, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o5882Field0, o5882Field1, o5882Field2)), o5205, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451)))
Load7791ARR8(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(java.lang.Object(Tree(o5882Field0, o5882Field1, o5882Field2)), o5205, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o5882Field0, o5882Field1, o5882Field2)), o5205, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451))) → Cond_Load7791ARR8(i1334 > 0 && i1253 > 0 && i1253 < i2 && i1255 > 0 && i1253 + 1 > 0, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(java.lang.Object(Tree(o5882Field0, o5882Field1, o5882Field2)), o5205, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o5882Field0, o5882Field1, o5882Field2)), o5205, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451)))
Cond_Load7791ARR8(TRUE, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(java.lang.Object(Tree(o5882Field0, o5882Field1, o5882Field2)), o5205, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o5882Field0, o5882Field1, o5882Field2)), o5205, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451))) → JMP10050(java.lang.Object(ARRAY(i2, a5234data)), i1253 + 1, i1255, java.lang.Object(Tree(java.lang.Object(Tree(o5882Field0, o5882Field1, o5882Field2)), o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5882Field0, o5882Field1, o5882Field2)))
JMP12465(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC)))) → Inc12523(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))))
Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(NULL, o5783, o5784))) → Load7791ARR9(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(NULL, o5783, o5784)), java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451)))
Load7791ARR9(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o5783, o5784)), java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451))) → Cond_Load7791ARR9(i1334 > 0 && i1253 > 0 && i1253 < i2 && i1255 > 0 && i1253 + 1 > 0, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o5783, o5784)), java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451)))
Cond_Load7791ARR9(TRUE, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o5783, o5784)), java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451))) → Inc12523(java.lang.Object(ARRAY(i2, a5234data)), i1253 + 1, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))))
Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, NULL, java.lang.Object(EOC))), java.lang.Object(Tree(o5204, NULL, java.lang.Object(EOC)))) → Load7791ARR10(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, NULL, java.lang.Object(EOC))), java.lang.Object(Tree(o5204, NULL, java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i1289, i1291, a5451)))
Load7791ARR10(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(Tree(o5204, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i1289, i1291, a5451))) → Cond_Load7791ARR10(i1253 > 0 && i1253 < i2 && i1255 > 0 && i1253 + 1 > 0, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(Tree(o5204, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i1289, i1291, a5451)))
Cond_Load7791ARR10(TRUE, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(Tree(o5204, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i1289, i1291, a5451))) → JMP12428(java.lang.Object(ARRAY(i2, a5234data)), i1253 + 1, i1255, java.lang.Object(Tree(o5204, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(Tree(o5204, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))))
Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(NULL, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(NULL, o5205, java.lang.Object(EOC)))) → Load7791ARR11(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(NULL, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(NULL, o5205, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451)))
Load7791ARR11(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o5205, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o5205, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451))) → Cond_Load7791ARR11(i1334 > 0 && i1253 > 0 && i1253 < i2 && i1255 > 0 && i1253 + 1 > 0, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o5205, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o5205, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451)))
Cond_Load7791ARR11(TRUE, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o5205, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o5205, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451))) → JMP12465(java.lang.Object(ARRAY(i2, a5234data)), i1253 + 1, i1255, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o5205, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o5205, java.lang.Object(EOC))))
The set Q consists of the following terms:
Load7791ARR4(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, java.lang.Object(Tree(x5, x6, x7)), java.lang.Object(EOC))), java.lang.Object(Tree(x4, java.lang.Object(Tree(x5, x6, x7)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, x8, x9, x10)))
Cond_Load7791ARR4(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, java.lang.Object(Tree(x5, x6, x7)), java.lang.Object(EOC))), java.lang.Object(Tree(x4, java.lang.Object(Tree(x5, x6, x7)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, x8, x9, x10)))
JMP10050(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, x7, x8)))
Load7791(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(x6, x7, x8)), x9, x10)))
Load7791ARR5(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(x6, x7, x8)), x9, x10)), java.lang.Object(java.lang.String(x11, x12, x13, x14)))
Cond_Load7791ARR5(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(x6, x7, x8)), x9, x10)), java.lang.Object(java.lang.String(x11, x12, x13, x14)))
Inc9967(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, x7, x8)))
Load7791(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, java.lang.Object(Tree(x7, x8, x9)), x10)))
Load7791ARR6(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, java.lang.Object(Tree(x7, x8, x9)), x10)), java.lang.Object(java.lang.String(0, x11, x12, x13)))
Cond_Load7791ARR6(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, java.lang.Object(Tree(x7, x8, x9)), x10)), java.lang.Object(java.lang.String(0, x11, x12, x13)))
Inc12523(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))))
JMP12428(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))))
Load7791(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, NULL, x7)))
Load7791ARR7(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x7)), java.lang.Object(java.lang.String(0, x8, x9, x10)))
Cond_Load7791ARR7(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x7)), java.lang.Object(java.lang.String(0, x8, x9, x10)))
Load7791ARR8(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(java.lang.Object(Tree(x4, x5, x6)), x7, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(x4, x5, x6)), x7, java.lang.Object(EOC))), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
Cond_Load7791ARR8(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(java.lang.Object(Tree(x4, x5, x6)), x7, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(x4, x5, x6)), x7, java.lang.Object(EOC))), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
JMP12465(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))))
Load7791(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(NULL, x6, x7)))
Load7791ARR9(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x6, x7)), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
Cond_Load7791ARR9(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x6, x7)), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
Load7791ARR10(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(Tree(x4, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, x5, x6, x7)))
Cond_Load7791ARR10(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(Tree(x4, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, x5, x6, x7)))
Load7791ARR11(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x4, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x4, java.lang.Object(EOC))), java.lang.Object(java.lang.String(x5, x6, x7, x8)))
Cond_Load7791ARR11(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x4, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x4, java.lang.Object(EOC))), java.lang.Object(java.lang.String(x5, x6, x7, x8)))

(21) DuplicateArgsRemoverProof (EQUIVALENT transformation)

Some arguments are removed because they only appear as duplicates.
We removed arguments according to the following replacements:

JMP12465(x1, x2, x3, x4, x5) → JMP12465(x1, x2, x3, x5)
Cond_Load7791ARR11(x1, x2, x3, x4, x5, x6, x7) → Cond_Load7791ARR11(x1, x2, x3, x4, x6, x7)
Load7791ARR11(x1, x2, x3, x4, x5, x6) → Load7791ARR11(x1, x2, x3, x5, x6)
JMP12428(x1, x2, x3, x4, x5) → JMP12428(x1, x2, x3, x5)
Cond_Load7791ARR10(x1, x2, x3, x4, x5, x6, x7) → Cond_Load7791ARR10(x1, x2, x3, x4, x6, x7)
Load7791ARR10(x1, x2, x3, x4, x5, x6) → Load7791ARR10(x1, x2, x3, x5, x6)
Inc12523(x1, x2, x3, x4, x5) → Inc12523(x1, x2, x3, x5)
Cond_Load7791ARR8(x1, x2, x3, x4, x5, x6, x7) → Cond_Load7791ARR8(x1, x2, x3, x4, x6, x7)
Load7791ARR8(x1, x2, x3, x4, x5, x6) → Load7791ARR8(x1, x2, x3, x5, x6)
Cond_Load7791ARR4(x1, x2, x3, x4, x5, x6, x7) → Cond_Load7791ARR4(x1, x2, x3, x4, x6, x7)
Load7791ARR4(x1, x2, x3, x4, x5, x6) → Load7791ARR4(x1, x2, x3, x5, x6)

(22) Obligation:

ITRS problem:

The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, java.lang.Object(Tree(o5839Field0, o5839Field1, o5839Field2)), java.lang.Object(EOC))), java.lang.Object(Tree(o5204, java.lang.Object(Tree(o5839Field0, o5839Field1, o5839Field2)), java.lang.Object(EOC)))) → Load7791ARR4(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, java.lang.Object(Tree(o5839Field0, o5839Field1, o5839Field2)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i1289, i1291, a5451)))
Load7791ARR4(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, java.lang.Object(Tree(o5839Field0, o5839Field1, o5839Field2)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i1289, i1291, a5451))) → Cond_Load7791ARR4(i1253 > 0 && i1253 < i2 && i1255 > 0 && i1253 + 1 > 0, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, java.lang.Object(Tree(o5839Field0, o5839Field1, o5839Field2)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i1289, i1291, a5451)))
Cond_Load7791ARR4(TRUE, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, java.lang.Object(Tree(o5839Field0, o5839Field1, o5839Field2)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i1289, i1291, a5451))) → Inc9967(java.lang.Object(ARRAY(i2, a5234data)), i1253 + 1, i1255, java.lang.Object(Tree(o5204, java.lang.Object(Tree(o5839Field0, o5839Field1, o5839Field2)), java.lang.Object(EOC))), java.lang.Object(Tree(o5839Field0, o5839Field1, o5839Field2)))
JMP10050(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5950Field0, o5950Field1, o5950Field2))) → Inc9967(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5950Field0, o5950Field1, o5950Field2)))
Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o5950Field0, o5950Field1, o5950Field2)), o5783, o5784))) → Load7791ARR5(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o5950Field0, o5950Field1, o5950Field2)), o5783, o5784)), java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451)))
Load7791ARR5(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o5950Field0, o5950Field1, o5950Field2)), o5783, o5784)), java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451))) → Cond_Load7791ARR5(i1334 > 0 && i1253 > 0 && i1253 < i2 && i1255 > 0 && i1253 + 1 > 0, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o5950Field0, o5950Field1, o5950Field2)), o5783, o5784)), java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451)))
Cond_Load7791ARR5(TRUE, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o5950Field0, o5950Field1, o5950Field2)), o5783, o5784)), java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451))) → Inc9967(java.lang.Object(ARRAY(i2, a5234data)), i1253 + 1, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5950Field0, o5950Field1, o5950Field2)))
Inc9967(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5931Field0, o5931Field1, o5931Field2))) → Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255 + -1, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5931Field0, o5931Field1, o5931Field2)))
Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5775, java.lang.Object(Tree(o5931Field0, o5931Field1, o5931Field2)), o5777))) → Load7791ARR6(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5775, java.lang.Object(Tree(o5931Field0, o5931Field1, o5931Field2)), o5777)), java.lang.Object(java.lang.String(0, i1289, i1291, a5451)))
Load7791ARR6(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5775, java.lang.Object(Tree(o5931Field0, o5931Field1, o5931Field2)), o5777)), java.lang.Object(java.lang.String(0, i1289, i1291, a5451))) → Cond_Load7791ARR6(i1253 > 0 && i1253 < i2 && i1255 > 0 && i1253 + 1 > 0, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5775, java.lang.Object(Tree(o5931Field0, o5931Field1, o5931Field2)), o5777)), java.lang.Object(java.lang.String(0, i1289, i1291, a5451)))
Cond_Load7791ARR6(TRUE, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5775, java.lang.Object(Tree(o5931Field0, o5931Field1, o5931Field2)), o5777)), java.lang.Object(java.lang.String(0, i1289, i1291, a5451))) → Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253 + 1, i1255 + -1, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5931Field0, o5931Field1, o5931Field2)))
Inc12523(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC)))) → Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255 + -1, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))))
JMP12428(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC)))) → Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255 + -1, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))))
Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5775, NULL, o5777))) → Load7791ARR7(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5775, NULL, o5777)), java.lang.Object(java.lang.String(0, i1289, i1291, a5451)))
Load7791ARR7(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5775, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o5777)), java.lang.Object(java.lang.String(0, i1289, i1291, a5451))) → Cond_Load7791ARR7(i1253 > 0 && i1253 < i2 && i1255 > 0 && i1253 + 1 > 0, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5775, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o5777)), java.lang.Object(java.lang.String(0, i1289, i1291, a5451)))
Cond_Load7791ARR7(TRUE, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5775, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o5777)), java.lang.Object(java.lang.String(0, i1289, i1291, a5451))) → Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253 + 1, i1255 + -1, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))))
Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(java.lang.Object(Tree(o5882Field0, o5882Field1, o5882Field2)), o5205, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o5882Field0, o5882Field1, o5882Field2)), o5205, java.lang.Object(EOC)))) → Load7791ARR8(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(java.lang.Object(Tree(o5882Field0, o5882Field1, o5882Field2)), o5205, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451)))
Load7791ARR8(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(java.lang.Object(Tree(o5882Field0, o5882Field1, o5882Field2)), o5205, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451))) → Cond_Load7791ARR8(i1334 > 0 && i1253 > 0 && i1253 < i2 && i1255 > 0 && i1253 + 1 > 0, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(java.lang.Object(Tree(o5882Field0, o5882Field1, o5882Field2)), o5205, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451)))
Cond_Load7791ARR8(TRUE, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(java.lang.Object(Tree(o5882Field0, o5882Field1, o5882Field2)), o5205, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451))) → JMP10050(java.lang.Object(ARRAY(i2, a5234data)), i1253 + 1, i1255, java.lang.Object(Tree(java.lang.Object(Tree(o5882Field0, o5882Field1, o5882Field2)), o5205, java.lang.Object(EOC))), java.lang.Object(Tree(o5882Field0, o5882Field1, o5882Field2)))
JMP12465(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC)))) → Inc12523(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))))
Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(NULL, o5783, o5784))) → Load7791ARR9(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(NULL, o5783, o5784)), java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451)))
Load7791ARR9(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o5783, o5784)), java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451))) → Cond_Load7791ARR9(i1334 > 0 && i1253 > 0 && i1253 < i2 && i1255 > 0 && i1253 + 1 > 0, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o5783, o5784)), java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451)))
Cond_Load7791ARR9(TRUE, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o5783, o5784)), java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451))) → Inc12523(java.lang.Object(ARRAY(i2, a5234data)), i1253 + 1, i1255, java.lang.Object(Tree(o5204, o5205, java.lang.Object(EOC))))
Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, NULL, java.lang.Object(EOC))), java.lang.Object(Tree(o5204, NULL, java.lang.Object(EOC)))) → Load7791ARR10(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, NULL, java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i1289, i1291, a5451)))
Load7791ARR10(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i1289, i1291, a5451))) → Cond_Load7791ARR10(i1253 > 0 && i1253 < i2 && i1255 > 0 && i1253 + 1 > 0, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i1289, i1291, a5451)))
Cond_Load7791ARR10(TRUE, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(o5204, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i1289, i1291, a5451))) → JMP12428(java.lang.Object(ARRAY(i2, a5234data)), i1253 + 1, i1255, java.lang.Object(Tree(o5204, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))))
Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(NULL, o5205, java.lang.Object(EOC))), java.lang.Object(Tree(NULL, o5205, java.lang.Object(EOC)))) → Load7791ARR11(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(NULL, o5205, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451)))
Load7791ARR11(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o5205, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451))) → Cond_Load7791ARR11(i1334 > 0 && i1253 > 0 && i1253 < i2 && i1255 > 0 && i1253 + 1 > 0, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o5205, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451)))
Cond_Load7791ARR11(TRUE, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o5205, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451))) → JMP12465(java.lang.Object(ARRAY(i2, a5234data)), i1253 + 1, i1255, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o5205, java.lang.Object(EOC))))
The set Q consists of the following terms:
Load7791ARR4(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, java.lang.Object(Tree(x5, x6, x7)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, x8, x9, x10)))
Cond_Load7791ARR4(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, java.lang.Object(Tree(x5, x6, x7)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, x8, x9, x10)))
JMP10050(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, x7, x8)))
Load7791(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(x6, x7, x8)), x9, x10)))
Load7791ARR5(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(x6, x7, x8)), x9, x10)), java.lang.Object(java.lang.String(x11, x12, x13, x14)))
Cond_Load7791ARR5(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(x6, x7, x8)), x9, x10)), java.lang.Object(java.lang.String(x11, x12, x13, x14)))
Inc9967(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, x7, x8)))
Load7791(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, java.lang.Object(Tree(x7, x8, x9)), x10)))
Load7791ARR6(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, java.lang.Object(Tree(x7, x8, x9)), x10)), java.lang.Object(java.lang.String(0, x11, x12, x13)))
Cond_Load7791ARR6(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, java.lang.Object(Tree(x7, x8, x9)), x10)), java.lang.Object(java.lang.String(0, x11, x12, x13)))
Inc12523(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))))
JMP12428(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))))
Load7791(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, NULL, x7)))
Load7791ARR7(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x7)), java.lang.Object(java.lang.String(0, x8, x9, x10)))
Cond_Load7791ARR7(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x7)), java.lang.Object(java.lang.String(0, x8, x9, x10)))
Load7791ARR8(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(java.lang.Object(Tree(x4, x5, x6)), x7, java.lang.Object(EOC))), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
Cond_Load7791ARR8(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(java.lang.Object(Tree(x4, x5, x6)), x7, java.lang.Object(EOC))), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
JMP12465(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))))
Load7791(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(NULL, x6, x7)))
Load7791ARR9(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x6, x7)), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
Cond_Load7791ARR9(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x6, x7)), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
Load7791ARR10(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, x5, x6, x7)))
Cond_Load7791ARR10(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, x5, x6, x7)))
Load7791ARR11(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x4, java.lang.Object(EOC))), java.lang.Object(java.lang.String(x5, x6, x7, x8)))
Cond_Load7791ARR11(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x4, java.lang.Object(EOC))), java.lang.Object(java.lang.String(x5, x6, x7, x8)))

(23) ITRSFilterProcessorProof (SOUND transformation)

We filter according the heuristic IdpCand1ShapeHeuristic
We removed arguments according to the following replacements:

Load7791(x1, x2, x3, x4, x5) → Load7791(x1, x2, x3)
Tree(x1, x2, x3) → Tree
Load7791ARR4(x1, x2, x3, x4, x5) → Load7791ARR4(x1, x2, x3)
Cond_Load7791ARR4(x1, x2, x3, x4, x5, x6) → Cond_Load7791ARR4(x1, x2, x3, x4)
Inc9967(x1, x2, x3, x4, x5) → Inc9967(x1, x2, x3)
JMP10050(x1, x2, x3, x4, x5) → JMP10050(x1, x2, x3)
Load7791ARR5(x1, x2, x3, x4, x5, x6) → Load7791ARR5(x1, x2, x3, x6)
Cond_Load7791ARR5(x1, x2, x3, x4, x5, x6, x7) → Cond_Load7791ARR5(x1, x2, x3, x4, x7)
Load7791ARR6(x1, x2, x3, x4, x5, x6) → Load7791ARR6(x1, x2, x3)
Cond_Load7791ARR6(x1, x2, x3, x4, x5, x6, x7) → Cond_Load7791ARR6(x1, x2, x3, x4)
Inc12523(x1, x2, x3, x4) → Inc12523(x1, x2, x3)
JMP12428(x1, x2, x3, x4) → JMP12428(x1, x2, x3)
Load7791ARR7(x1, x2, x3, x4, x5, x6) → Load7791ARR7(x1, x2, x3)
Cond_Load7791ARR7(x1, x2, x3, x4, x5, x6, x7) → Cond_Load7791ARR7(x1, x2, x3, x4)
Load7791ARR8(x1, x2, x3, x4, x5) → Load7791ARR8(x1, x2, x3, x5)
Cond_Load7791ARR8(x1, x2, x3, x4, x5, x6) → Cond_Load7791ARR8(x1, x2, x3, x4, x6)
JMP12465(x1, x2, x3, x4) → JMP12465(x1, x2, x3)
Load7791ARR9(x1, x2, x3, x4, x5, x6) → Load7791ARR9(x1, x2, x3, x6)
Cond_Load7791ARR9(x1, x2, x3, x4, x5, x6, x7) → Cond_Load7791ARR9(x1, x2, x3, x4, x7)
Load7791ARR10(x1, x2, x3, x4, x5) → Load7791ARR10(x1, x2, x3)
Cond_Load7791ARR10(x1, x2, x3, x4, x5, x6) → Cond_Load7791ARR10(x1, x2, x3, x4)
Load7791ARR11(x1, x2, x3, x4, x5) → Load7791ARR11(x1, x2, x3, x5)
Cond_Load7791ARR11(x1, x2, x3, x4, x5, x6) → Cond_Load7791ARR11(x1, x2, x3, x4, x6)

(24) Obligation:

ITRS problem:

The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255) → Load7791ARR4(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255)
Load7791ARR4(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255) → Cond_Load7791ARR4(i1253 > 0 && i1253 < i2 && i1255 > 0 && i1253 + 1 > 0, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255)
Cond_Load7791ARR4(TRUE, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255) → Inc9967(java.lang.Object(ARRAY(i2, a5234data)), i1253 + 1, i1255)
JMP10050(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255) → Inc9967(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255)
Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255) → Load7791ARR5(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451)))
Load7791ARR5(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451))) → Cond_Load7791ARR5(i1334 > 0 && i1253 > 0 && i1253 < i2 && i1255 > 0 && i1253 + 1 > 0, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451)))
Cond_Load7791ARR5(TRUE, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451))) → Inc9967(java.lang.Object(ARRAY(i2, a5234data)), i1253 + 1, i1255)
Inc9967(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255) → Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255 + -1)
Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255) → Load7791ARR6(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255)
Load7791ARR6(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255) → Cond_Load7791ARR6(i1253 > 0 && i1253 < i2 && i1255 > 0 && i1253 + 1 > 0, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255)
Cond_Load7791ARR6(TRUE, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255) → Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253 + 1, i1255 + -1)
Inc12523(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255) → Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255 + -1)
JMP12428(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255) → Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255 + -1)
Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255) → Load7791ARR7(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255)
Load7791ARR7(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255) → Cond_Load7791ARR7(i1253 > 0 && i1253 < i2 && i1255 > 0 && i1253 + 1 > 0, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255)
Cond_Load7791ARR7(TRUE, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255) → Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253 + 1, i1255 + -1)
Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255) → Load7791ARR8(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451)))
Load7791ARR8(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451))) → Cond_Load7791ARR8(i1334 > 0 && i1253 > 0 && i1253 < i2 && i1255 > 0 && i1253 + 1 > 0, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451)))
Cond_Load7791ARR8(TRUE, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451))) → JMP10050(java.lang.Object(ARRAY(i2, a5234data)), i1253 + 1, i1255)
JMP12465(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255) → Inc12523(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255)
Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255) → Load7791ARR9(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451)))
Load7791ARR9(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451))) → Cond_Load7791ARR9(i1334 > 0 && i1253 > 0 && i1253 < i2 && i1255 > 0 && i1253 + 1 > 0, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451)))
Cond_Load7791ARR9(TRUE, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451))) → Inc12523(java.lang.Object(ARRAY(i2, a5234data)), i1253 + 1, i1255)
Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255) → Load7791ARR10(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255)
Load7791ARR10(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255) → Cond_Load7791ARR10(i1253 > 0 && i1253 < i2 && i1255 > 0 && i1253 + 1 > 0, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255)
Cond_Load7791ARR10(TRUE, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255) → JMP12428(java.lang.Object(ARRAY(i2, a5234data)), i1253 + 1, i1255)
Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255) → Load7791ARR11(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451)))
Load7791ARR11(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451))) → Cond_Load7791ARR11(i1334 > 0 && i1253 > 0 && i1253 < i2 && i1255 > 0 && i1253 + 1 > 0, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451)))
Cond_Load7791ARR11(TRUE, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451))) → JMP12465(java.lang.Object(ARRAY(i2, a5234data)), i1253 + 1, i1255)
The set Q consists of the following terms:
Load7791(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load7791ARR4(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load7791ARR4(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
JMP10050(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load7791ARR5(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load7791ARR5(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Inc9967(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load7791ARR6(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load7791ARR6(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
Inc12523(java.lang.Object(ARRAY(x0, x1)), x2, x3)
JMP12428(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load7791ARR7(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load7791ARR7(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load7791ARR8(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load7791ARR8(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
JMP12465(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load7791ARR9(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load7791ARR9(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Load7791ARR10(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load7791ARR10(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load7791ARR11(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load7791ARR11(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))

(25) ITRSFSMergerProof (SOUND transformation)

The following function symbols have been merged:

Load7791ARR4, Load7791ARR10	>	Load7791ARR4_3
Load7791ARR6, Load7791ARR7	>	Load7791ARR6_3
Cond_Load7791ARR4, Cond_Load7791ARR10	>	Cond_Load7791ARR4_4
JMP10050, JMP12465	>	JMP10050_3
Load7791ARR5, Load7791ARR9	>	Load7791ARR5_4
Load7791ARR8, Load7791ARR11	>	Load7791ARR8_4
Cond_Load7791ARR8, Cond_Load7791ARR11	>	Cond_Load7791ARR8_5
Cond_Load7791ARR5, Cond_Load7791ARR9	>	Cond_Load7791ARR5_5
Inc9967, Inc12523, JMP12428	>	Inc9967_3
Cond_Load7791ARR6, Cond_Load7791ARR7	>	Cond_Load7791ARR6_4

(26) Obligation:

ITRS problem:

The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

(27) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

(28) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

The ITRS R consists of the following rules:
Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255) → Load7791ARR4(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255)
Load7791ARR4(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255) → Cond_Load7791ARR4(i1253 > 0 && i1253 < i2 && i1255 > 0 && i1253 + 1 > 0, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255)
Cond_Load7791ARR4(TRUE, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255) → Inc9967(java.lang.Object(ARRAY(i2, a5234data)), i1253 + 1, i1255)
JMP10050(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255) → Inc9967(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255)
Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255) → Load7791ARR5(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451)))
Load7791ARR5(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451))) → Cond_Load7791ARR5(i1334 > 0 && i1253 > 0 && i1253 < i2 && i1255 > 0 && i1253 + 1 > 0, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451)))
Cond_Load7791ARR5(TRUE, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451))) → Inc9967(java.lang.Object(ARRAY(i2, a5234data)), i1253 + 1, i1255)
Inc9967(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255) → Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1268, i1255 + -1)
Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255) → Load7791ARR6(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255)
Load7791ARR6(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255) → Cond_Load7791ARR6(i1253 > 0 && i1253 < i2 && i1255 > 0 && i1253 + 1 > 0, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255)
Cond_Load7791ARR6(TRUE, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255) → Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253 + 1, i1255 + -1)
Load7791(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255) → Load7791ARR8(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451)))
Load7791ARR8(java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451))) → Cond_Load7791ARR8(i1334 > 0 && i1253 > 0 && i1253 < i2 && i1255 > 0 && i1253 + 1 > 0, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451)))
Cond_Load7791ARR8(TRUE, java.lang.Object(ARRAY(i2, a5234data)), i1253, i1255, java.lang.Object(java.lang.String(i1334, i1289, i1291, a5451))) → JMP10050(java.lang.Object(ARRAY(i2, a5234data)), i1253 + 1, i1255)

The integer pair graph contains the following rules and edges:
(0): LOAD7791(java.lang.Object(ARRAY(i2[0], a5234data[0])), i1253[0], i1255[0]) → LOAD7791ARR4(java.lang.Object(ARRAY(i2[0], a5234data[0])), i1253[0], i1255[0])
(1): LOAD7791ARR4(java.lang.Object(ARRAY(i2[1], a5234data[1])), i1253[1], i1255[1]) → COND_LOAD7791ARR4(i1253[1] > 0 && i1253[1] < i2[1] && i1255[1] > 0 && i1253[1] + 1 > 0, java.lang.Object(ARRAY(i2[1], a5234data[1])), i1253[1], i1255[1])
(2): COND_LOAD7791ARR4(TRUE, java.lang.Object(ARRAY(i2[2], a5234data[2])), i1253[2], i1255[2]) → INC9967(java.lang.Object(ARRAY(i2[2], a5234data[2])), i1253[2] + 1, i1255[2])
(3): JMP10050'(java.lang.Object(ARRAY(i2[3], a5234data[3])), i1268[3], i1255[3]) → INC9967(java.lang.Object(ARRAY(i2[3], a5234data[3])), i1268[3], i1255[3])
(4): LOAD7791(java.lang.Object(ARRAY(i2[4], a5234data[4])), i1253[4], i1255[4]) → LOAD7791ARR5(java.lang.Object(ARRAY(i2[4], a5234data[4])), i1253[4], i1255[4], java.lang.Object(java.lang.String(i1334[4], i1289[4], i1291[4], a5451[4])))
(5): LOAD7791ARR5(java.lang.Object(ARRAY(i2[5], a5234data[5])), i1253[5], i1255[5], java.lang.Object(java.lang.String(i1334[5], i1289[5], i1291[5], a5451[5]))) → COND_LOAD7791ARR5(i1334[5] > 0 && i1253[5] > 0 && i1253[5] < i2[5] && i1255[5] > 0 && i1253[5] + 1 > 0, java.lang.Object(ARRAY(i2[5], a5234data[5])), i1253[5], i1255[5], java.lang.Object(java.lang.String(i1334[5], i1289[5], i1291[5], a5451[5])))
(6): COND_LOAD7791ARR5(TRUE, java.lang.Object(ARRAY(i2[6], a5234data[6])), i1253[6], i1255[6], java.lang.Object(java.lang.String(i1334[6], i1289[6], i1291[6], a5451[6]))) → INC9967(java.lang.Object(ARRAY(i2[6], a5234data[6])), i1253[6] + 1, i1255[6])
(7): INC9967(java.lang.Object(ARRAY(i2[7], a5234data[7])), i1268[7], i1255[7]) → LOAD7791(java.lang.Object(ARRAY(i2[7], a5234data[7])), i1268[7], i1255[7] + -1)
(8): LOAD7791(java.lang.Object(ARRAY(i2[8], a5234data[8])), i1253[8], i1255[8]) → LOAD7791ARR6(java.lang.Object(ARRAY(i2[8], a5234data[8])), i1253[8], i1255[8])
(9): LOAD7791ARR6(java.lang.Object(ARRAY(i2[9], a5234data[9])), i1253[9], i1255[9]) → COND_LOAD7791ARR6(i1253[9] > 0 && i1253[9] < i2[9] && i1255[9] > 0 && i1253[9] + 1 > 0, java.lang.Object(ARRAY(i2[9], a5234data[9])), i1253[9], i1255[9])
(10): COND_LOAD7791ARR6(TRUE, java.lang.Object(ARRAY(i2[10], a5234data[10])), i1253[10], i1255[10]) → LOAD7791(java.lang.Object(ARRAY(i2[10], a5234data[10])), i1253[10] + 1, i1255[10] + -1)
(11): LOAD7791(java.lang.Object(ARRAY(i2[11], a5234data[11])), i1253[11], i1255[11]) → LOAD7791ARR8(java.lang.Object(ARRAY(i2[11], a5234data[11])), i1253[11], i1255[11], java.lang.Object(java.lang.String(i1334[11], i1289[11], i1291[11], a5451[11])))
(12): LOAD7791ARR8(java.lang.Object(ARRAY(i2[12], a5234data[12])), i1253[12], i1255[12], java.lang.Object(java.lang.String(i1334[12], i1289[12], i1291[12], a5451[12]))) → COND_LOAD7791ARR8(i1334[12] > 0 && i1253[12] > 0 && i1253[12] < i2[12] && i1255[12] > 0 && i1253[12] + 1 > 0, java.lang.Object(ARRAY(i2[12], a5234data[12])), i1253[12], i1255[12], java.lang.Object(java.lang.String(i1334[12], i1289[12], i1291[12], a5451[12])))
(13): COND_LOAD7791ARR8(TRUE, java.lang.Object(ARRAY(i2[13], a5234data[13])), i1253[13], i1255[13], java.lang.Object(java.lang.String(i1334[13], i1289[13], i1291[13], a5451[13]))) → JMP10050'(java.lang.Object(ARRAY(i2[13], a5234data[13])), i1253[13] + 1, i1255[13])

(0) -> (1), if ((i1253[0] →^* i1253[1])∧(java.lang.Object(ARRAY(i2[0], a5234data[0])) →^* java.lang.Object(ARRAY(i2[1], a5234data[1])))∧(i1255[0] →^* i1255[1]))

(1) -> (2), if ((i1253[1] > 0 && i1253[1] < i2[1] && i1255[1] > 0 && i1253[1] + 1 > 0 →^* TRUE)∧(i1253[1] →^* i1253[2])∧(java.lang.Object(ARRAY(i2[1], a5234data[1])) →^* java.lang.Object(ARRAY(i2[2], a5234data[2])))∧(i1255[1] →^* i1255[2]))

(2) -> (7), if ((i1253[2] + 1 →^* i1268[7])∧(java.lang.Object(ARRAY(i2[2], a5234data[2])) →^* java.lang.Object(ARRAY(i2[7], a5234data[7])))∧(i1255[2] →^* i1255[7]))

(3) -> (7), if ((i1268[3] →^* i1268[7])∧(i1255[3] →^* i1255[7])∧(java.lang.Object(ARRAY(i2[3], a5234data[3])) →^* java.lang.Object(ARRAY(i2[7], a5234data[7]))))

(4) -> (5), if ((i1253[4] →^* i1253[5])∧(java.lang.Object(ARRAY(i2[4], a5234data[4])) →^* java.lang.Object(ARRAY(i2[5], a5234data[5])))∧(java.lang.Object(java.lang.String(i1334[4], i1289[4], i1291[4], a5451[4])) →^* java.lang.Object(java.lang.String(i1334[5], i1289[5], i1291[5], a5451[5])))∧(i1255[4] →^* i1255[5]))

(5) -> (6), if ((java.lang.Object(ARRAY(i2[5], a5234data[5])) →^* java.lang.Object(ARRAY(i2[6], a5234data[6])))∧(i1334[5] > 0 && i1253[5] > 0 && i1253[5] < i2[5] && i1255[5] > 0 && i1253[5] + 1 > 0 →^* TRUE)∧(i1255[5] →^* i1255[6])∧(i1253[5] →^* i1253[6])∧(java.lang.Object(java.lang.String(i1334[5], i1289[5], i1291[5], a5451[5])) →^* java.lang.Object(java.lang.String(i1334[6], i1289[6], i1291[6], a5451[6]))))

(6) -> (7), if ((i1253[6] + 1 →^* i1268[7])∧(java.lang.Object(ARRAY(i2[6], a5234data[6])) →^* java.lang.Object(ARRAY(i2[7], a5234data[7])))∧(i1255[6] →^* i1255[7]))

(7) -> (0), if ((i1255[7] + -1 →^* i1255[0])∧(i1268[7] →^* i1253[0])∧(java.lang.Object(ARRAY(i2[7], a5234data[7])) →^* java.lang.Object(ARRAY(i2[0], a5234data[0]))))

(7) -> (4), if ((i1255[7] + -1 →^* i1255[4])∧(i1268[7] →^* i1253[4])∧(java.lang.Object(ARRAY(i2[7], a5234data[7])) →^* java.lang.Object(ARRAY(i2[4], a5234data[4]))))

(7) -> (8), if ((i1255[7] + -1 →^* i1255[8])∧(java.lang.Object(ARRAY(i2[7], a5234data[7])) →^* java.lang.Object(ARRAY(i2[8], a5234data[8])))∧(i1268[7] →^* i1253[8]))

(7) -> (11), if ((java.lang.Object(ARRAY(i2[7], a5234data[7])) →^* java.lang.Object(ARRAY(i2[11], a5234data[11])))∧(i1268[7] →^* i1253[11])∧(i1255[7] + -1 →^* i1255[11]))

(8) -> (9), if ((i1253[8] →^* i1253[9])∧(java.lang.Object(ARRAY(i2[8], a5234data[8])) →^* java.lang.Object(ARRAY(i2[9], a5234data[9])))∧(i1255[8] →^* i1255[9]))

(9) -> (10), if ((i1255[9] →^* i1255[10])∧(i1253[9] > 0 && i1253[9] < i2[9] && i1255[9] > 0 && i1253[9] + 1 > 0 →^* TRUE)∧(i1253[9] →^* i1253[10])∧(java.lang.Object(ARRAY(i2[9], a5234data[9])) →^* java.lang.Object(ARRAY(i2[10], a5234data[10]))))

(10) -> (0), if ((i1253[10] + 1 →^* i1253[0])∧(java.lang.Object(ARRAY(i2[10], a5234data[10])) →^* java.lang.Object(ARRAY(i2[0], a5234data[0])))∧(i1255[10] + -1 →^* i1255[0]))

(10) -> (4), if ((i1255[10] + -1 →^* i1255[4])∧(java.lang.Object(ARRAY(i2[10], a5234data[10])) →^* java.lang.Object(ARRAY(i2[4], a5234data[4])))∧(i1253[10] + 1 →^* i1253[4]))

(10) -> (8), if ((i1253[10] + 1 →^* i1253[8])∧(java.lang.Object(ARRAY(i2[10], a5234data[10])) →^* java.lang.Object(ARRAY(i2[8], a5234data[8])))∧(i1255[10] + -1 →^* i1255[8]))

(10) -> (11), if ((i1255[10] + -1 →^* i1255[11])∧(i1253[10] + 1 →^* i1253[11])∧(java.lang.Object(ARRAY(i2[10], a5234data[10])) →^* java.lang.Object(ARRAY(i2[11], a5234data[11]))))

(11) -> (12), if ((java.lang.Object(ARRAY(i2[11], a5234data[11])) →^* java.lang.Object(ARRAY(i2[12], a5234data[12])))∧(java.lang.Object(java.lang.String(i1334[11], i1289[11], i1291[11], a5451[11])) →^* java.lang.Object(java.lang.String(i1334[12], i1289[12], i1291[12], a5451[12])))∧(i1255[11] →^* i1255[12])∧(i1253[11] →^* i1253[12]))

(12) -> (13), if ((java.lang.Object(java.lang.String(i1334[12], i1289[12], i1291[12], a5451[12])) →^* java.lang.Object(java.lang.String(i1334[13], i1289[13], i1291[13], a5451[13])))∧(i1334[12] > 0 && i1253[12] > 0 && i1253[12] < i2[12] && i1255[12] > 0 && i1253[12] + 1 > 0 →^* TRUE)∧(i1253[12] →^* i1253[13])∧(i1255[12] →^* i1255[13])∧(java.lang.Object(ARRAY(i2[12], a5234data[12])) →^* java.lang.Object(ARRAY(i2[13], a5234data[13]))))

(13) -> (3), if ((java.lang.Object(ARRAY(i2[13], a5234data[13])) →^* java.lang.Object(ARRAY(i2[3], a5234data[3])))∧(i1253[13] + 1 →^* i1268[3])∧(i1255[13] →^* i1255[3]))

The set Q consists of the following terms:
Load7791(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load7791ARR4(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load7791ARR4(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
JMP10050(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load7791ARR5(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load7791ARR5(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Inc9967(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load7791ARR6(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load7791ARR6(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load7791ARR8(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load7791ARR8(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))

(29) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(30) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD7791(java.lang.Object(ARRAY(i2[0], a5234data[0])), i1253[0], i1255[0]) → LOAD7791ARR4(java.lang.Object(ARRAY(i2[0], a5234data[0])), i1253[0], i1255[0])
(1): LOAD7791ARR4(java.lang.Object(ARRAY(i2[1], a5234data[1])), i1253[1], i1255[1]) → COND_LOAD7791ARR4(i1253[1] > 0 && i1253[1] < i2[1] && i1255[1] > 0 && i1253[1] + 1 > 0, java.lang.Object(ARRAY(i2[1], a5234data[1])), i1253[1], i1255[1])
(2): COND_LOAD7791ARR4(TRUE, java.lang.Object(ARRAY(i2[2], a5234data[2])), i1253[2], i1255[2]) → INC9967(java.lang.Object(ARRAY(i2[2], a5234data[2])), i1253[2] + 1, i1255[2])
(3): JMP10050'(java.lang.Object(ARRAY(i2[3], a5234data[3])), i1268[3], i1255[3]) → INC9967(java.lang.Object(ARRAY(i2[3], a5234data[3])), i1268[3], i1255[3])
(4): LOAD7791(java.lang.Object(ARRAY(i2[4], a5234data[4])), i1253[4], i1255[4]) → LOAD7791ARR5(java.lang.Object(ARRAY(i2[4], a5234data[4])), i1253[4], i1255[4], java.lang.Object(java.lang.String(i1334[4], i1289[4], i1291[4], a5451[4])))
(5): LOAD7791ARR5(java.lang.Object(ARRAY(i2[5], a5234data[5])), i1253[5], i1255[5], java.lang.Object(java.lang.String(i1334[5], i1289[5], i1291[5], a5451[5]))) → COND_LOAD7791ARR5(i1334[5] > 0 && i1253[5] > 0 && i1253[5] < i2[5] && i1255[5] > 0 && i1253[5] + 1 > 0, java.lang.Object(ARRAY(i2[5], a5234data[5])), i1253[5], i1255[5], java.lang.Object(java.lang.String(i1334[5], i1289[5], i1291[5], a5451[5])))
(6): COND_LOAD7791ARR5(TRUE, java.lang.Object(ARRAY(i2[6], a5234data[6])), i1253[6], i1255[6], java.lang.Object(java.lang.String(i1334[6], i1289[6], i1291[6], a5451[6]))) → INC9967(java.lang.Object(ARRAY(i2[6], a5234data[6])), i1253[6] + 1, i1255[6])
(7): INC9967(java.lang.Object(ARRAY(i2[7], a5234data[7])), i1268[7], i1255[7]) → LOAD7791(java.lang.Object(ARRAY(i2[7], a5234data[7])), i1268[7], i1255[7] + -1)
(8): LOAD7791(java.lang.Object(ARRAY(i2[8], a5234data[8])), i1253[8], i1255[8]) → LOAD7791ARR6(java.lang.Object(ARRAY(i2[8], a5234data[8])), i1253[8], i1255[8])
(9): LOAD7791ARR6(java.lang.Object(ARRAY(i2[9], a5234data[9])), i1253[9], i1255[9]) → COND_LOAD7791ARR6(i1253[9] > 0 && i1253[9] < i2[9] && i1255[9] > 0 && i1253[9] + 1 > 0, java.lang.Object(ARRAY(i2[9], a5234data[9])), i1253[9], i1255[9])
(10): COND_LOAD7791ARR6(TRUE, java.lang.Object(ARRAY(i2[10], a5234data[10])), i1253[10], i1255[10]) → LOAD7791(java.lang.Object(ARRAY(i2[10], a5234data[10])), i1253[10] + 1, i1255[10] + -1)
(11): LOAD7791(java.lang.Object(ARRAY(i2[11], a5234data[11])), i1253[11], i1255[11]) → LOAD7791ARR8(java.lang.Object(ARRAY(i2[11], a5234data[11])), i1253[11], i1255[11], java.lang.Object(java.lang.String(i1334[11], i1289[11], i1291[11], a5451[11])))
(12): LOAD7791ARR8(java.lang.Object(ARRAY(i2[12], a5234data[12])), i1253[12], i1255[12], java.lang.Object(java.lang.String(i1334[12], i1289[12], i1291[12], a5451[12]))) → COND_LOAD7791ARR8(i1334[12] > 0 && i1253[12] > 0 && i1253[12] < i2[12] && i1255[12] > 0 && i1253[12] + 1 > 0, java.lang.Object(ARRAY(i2[12], a5234data[12])), i1253[12], i1255[12], java.lang.Object(java.lang.String(i1334[12], i1289[12], i1291[12], a5451[12])))
(13): COND_LOAD7791ARR8(TRUE, java.lang.Object(ARRAY(i2[13], a5234data[13])), i1253[13], i1255[13], java.lang.Object(java.lang.String(i1334[13], i1289[13], i1291[13], a5451[13]))) → JMP10050'(java.lang.Object(ARRAY(i2[13], a5234data[13])), i1253[13] + 1, i1255[13])